/*
 * Copyright (c) 2013, SRI International
 * All rights reserved.
 * Licensed under the The BSD 3-Clause License;
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at:
 * 
 * http://opensource.org/licenses/BSD-3-Clause
 * 
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions
 * are met:
 * 
 * Redistributions of source code must retain the above copyright
 * notice, this list of conditions and the following disclaimer.
 * 
 * Redistributions in binary form must reproduce the above copyright
 * notice, this list of conditions and the following disclaimer in the
 * documentation and/or other materials provided with the distribution.
 * 
 * Neither the name of the aic-expresso nor the names of its
 * contributors may be used to endorse or promote products derived from
 * this software without specific prior written permission.
 * 
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
 * FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
 * COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, 
 * INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES 
 * (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) 
 * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, 
 * STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) 
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED
 * OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.sri.ai.test.grinder.library.equality.cardinality;

import java.util.ArrayList;
import java.util.List;

import com.sri.ai.expresso.api.Expression;
import com.sri.ai.grinder.api.RewritingProcess;
import com.sri.ai.grinder.library.DirectCardinalityComputationFactory;
import com.sri.ai.grinder.library.boole.core.SimpleFormulaGenerator;

public class RandomCardinalityStressIT extends AbstractCardinalityRewriterStressTests {
	private SimpleFormulaGenerator gn = new SimpleFormulaGenerator(20, 20);  // with 20 variables and 20 constants
	
	private boolean ADD_PRE_GENERATED_FORMULAS = false;
	private boolean ADD_GENERAL_FORMULAS = false;
	private boolean ADD_CONJUNCTION_OF_DISEQUALITIES = false;
	private boolean ADD_CNF_FORMULAS = false;
	private boolean ADD_DNF_FORMULAS = true;
	private boolean GENERATE_FORMULAS_WITH_FREE_VARIABLES = false;
	
	public List<CardinalityRewriter> makeCardinalityRewriters() {
		List<CardinalityRewriter> result = super.makeCardinalityRewriters();
		
		result.add(new DefaultCardinalityRewriter("Direct Cardinality Rewriter",
				new CardinalityRewriteProcessFactory() {
					@Override
					public RewritingProcess newInstance(Expression rootExpression, RewritingProcess parentProcess) {
						return DirectCardinalityComputationFactory.newCardinalityProcess(rootExpression, parentProcess);
					}
				}, 
				com.sri.ai.grinder.library.equality.cardinality.direct.CardinalityRewriter.R_card,
				_sharedCountsDeclaration, _numberRewritesToAverage));
		
		return result;
	}	

	@Override
	public List<CardinalityStressTest> makeCardinalityStressTests() {
		List<CardinalityStressTest> result = super.makeCardinalityStressTests();
		if ( ADD_PRE_GENERATED_FORMULAS ) {
			addPreGeneratedTests(result);
		}
		if ( ADD_GENERAL_FORMULAS ) {
			generateAndAddNewGeneralFormulas(result, GENERATE_FORMULAS_WITH_FREE_VARIABLES);
		}
		if ( ADD_CONJUNCTION_OF_DISEQUALITIES ) {
			generateAndAddNewConjunctionOfDisequalities(result, GENERATE_FORMULAS_WITH_FREE_VARIABLES);
		}
		if ( ADD_CNF_FORMULAS ) {
			generateAndAddNewCNFFormulas(result, GENERATE_FORMULAS_WITH_FREE_VARIABLES);
		}
		if ( ADD_DNF_FORMULAS ) {
			generateAndAddNewDNFFormulas(result, GENERATE_FORMULAS_WITH_FREE_VARIABLES);
		}
		return result;
	}
	
	private void generateAndAddNewGeneralFormulas(List<CardinalityStressTest> result, boolean withPossibleFreeVariables) {
		List<String> newTests = new ArrayList<String>();
		for (int i = 30; i<60; i+= 3) {
			Expression formula = gn.generateRandomFormulas(i);
			Expression ex = gn.generateRandomCardinality(formula, withPossibleFreeVariables);
			newTests.add(writer.toString(ex));
		}
		result.add(new CannedFormulaStressTest("Randomly genrated formulas", newTests.toArray(new String[0])));
	}	
	
	private void generateAndAddNewConjunctionOfDisequalities(List<CardinalityStressTest> result, boolean withPossibleFreeVariables) {
		List<String> newTests = new ArrayList<String>();
		for (int i = 30; i<90; i+=3) {
			Expression formula = gn.generateConjunctionOfDisequalities(30);
			Expression ex = gn.generateRandomCardinality(formula, withPossibleFreeVariables);
			newTests.add(writer.toString(ex));
		}
		result.add(new CannedFormulaStressTest("Randomly genrated conjunctions of disequalities", newTests.toArray(new String[0])));
	}	
	
	private void generateAndAddNewCNFFormulas(List<CardinalityStressTest> result, boolean withPossibleFreeVariables) {
		List<String> newTests = new ArrayList<String>();
		for (int i = 20; i<60; i+= 3) {
			Expression formula = gn.generateCNF(i, i);
			Expression ex = gn.generateRandomCardinality(formula, withPossibleFreeVariables);
			newTests.add(writer.toString(ex));
		}		
		result.add(new CannedFormulaStressTest("Randomly genrated CNF formulas", newTests.toArray(new String[0])));
	}	
	
	private void generateAndAddNewDNFFormulas(List<CardinalityStressTest> result, boolean withPossibleFreeVariables) {
		List<String> newTests = new ArrayList<String>();
		for (int i = 20; i<60; i+= 3) {
			Expression formula = gn.generateDNF(i, i);
			Expression ex = gn.generateRandomCardinality(formula, withPossibleFreeVariables);
			newTests.add(writer.toString(ex));
		}		
		result.add(new CannedFormulaStressTest("Randomly genrated DNF formulas", newTests.toArray(new String[0])));
	}	
	
	private void addPreGeneratedTests(List<CardinalityStressTest> result) {
		result.add(new CannedFormulaStressTest("Randomly pre-genrated formulas by SimpleFormulaGenerator", new String[] {
			"| { ( on X2, X3, X10, X4, X14, X13, X9, X18, X19, X15 ) ( X2, X3, X10, X4, X14, X13, X9, X18, X19, X15 ) | (X19 = X13 and a9 = X2 and a3 = a10 => a11 = a2 or false or X4 != a19) => (a6 = a13 and (X9 != X10 or X15 = a10) and X9 != a13 => X14 != X3 and X18 != a17 and a4 = a14) } |",
			"| { ( on X1, X2, X10, X5, X6, X14, X13, X12, X11, X17, X16, X15, X9, X8 ) ( X1, X2, X10, X5, X6, X14, X13, X12, X11, X17, X16, X15, X9, X8 ) | a9 != X11 and X15 != X1 and X17 != X8 or a11 != X14 and a17 != X16 and X14 = a18 and X13 = X1 or a20 = a9 or X11 = X1 and X9 != X11 and a3 != X17 and X8 = X10 and X13 != a7 or a10 = a14 and a20 = X14 and X10 = X14 and X12 = X6 and X2 = X5 or a12 != X8 and X1 != a2 and a15 != X6 } |",
			"| { ( on X1, X2, X3, X4, X5, X6, X14, X20, X11, X17, X16, X15, X9 ) ( X1, X2, X3, X4, X5, X6, X14, X20, X11, X17, X16, X15, X9 ) | a1 != X4 and a3 != X5 and a19 = a6 or a17 != X16 and X14 = X3 and a18 != a6 or a3 = X15 and a4 != X17 or X1 != X6 and a3 = X1 <=> (a17 = X11 or X1 != X15 and X2 = a9 or X15 = X9 => false and X20 = X16 or a2 != a12 and a11 = a4 or X6 = a2) } |",
			"| { ( on X1, X2, X3, X4, X5, X6, X7, X14, X13, X20, X12, X11, X16, X15, X9, X8, X19 ) ( X1, X2, X3, X4, X5, X6, X7, X14, X13, X20, X12, X11, X16, X15, X9, X8, X19 ) | (X13 != a8 or a19 != a1 or X3 != X5 or X8 = X20 or X4 != X2) and X12 = X16 and (X7 != X5 or a6 = a8 or a17 != X20) and (X14 = a7 or a3 != X20 or a20 = a11) and (X20 = a12 or X16 = a12 or a5 != X16 or a20 != X1) and X15 = X4 and (X6 = X9 or X19 = a13 or X15 = X5 or X11 != a13 or X7 = X20) } |",
			"| { ( on X1, X3, X4, X5, X6, X7, X20, X12, X11, X18, X17, X16, X15, X9 ) ( X1, X3, X4, X5, X6, X7, X20, X12, X11, X18, X17, X16, X15, X9 ) | a7 != X7 and (X6 != a14 or X7 = X5) and (a20 = X20 or X11 = X15) and (X7 = a2 or a14 != a9) and a10 = a2 <=> (X3 != X17 or X16 = a9 or X12 != a2) and (a1 != X4 or X11 != X18 or a7 = a12 or X7 = X5) and (a17 != X20 or X9 = a4 or X18 != a17) and (a8 = a19 or X5 = X15 or a6 != a5) and X11 = X1 } |",
			"| { ( on X1, X2, X3, X4, X5, X7, X14, X13, X12, X11, X17, X16, X15, X9, X19 ) ( X1, X2, X3, X4, X5, X7, X14, X13, X12, X11, X17, X16, X15, X9, X19 ) | (X11 = a16 or X11 = a11 or X16 = X2 or a6 = X3 or a2 = X1) and (X2 != a1 or X12 != X16 or a17 != X1) and (X1 != a10 or X15 = X2 or X14 != a11 or X15 != X7 or a7 != X13) and (X13 = a4 or X4 = a12 or a17 = a14 or a20 = a18 or X2 != a14 or X3 != X9) and (a16 = a18 or a20 = a4) and (X15 = a14 or X9 != a2 or a14 != X17 or X5 = X3 or a16 != X2 or X1 != a15) and a18 != X19 } |",
			"| { ( on X1, X2, X3, X4, X5, X7, X14, X20, X11, X18, X17, X16, X8 ) ( X1, X2, X3, X4, X5, X7, X14, X20, X11, X18, X17, X16, X8 ) | (a4 = X20 or a7 = X1 or X8 = a19) and (a6 = a9 or a5 != a9 or X14 = X1 or X5 = a9) and (a14 = a20 or X4 != X7 or X18 = X16 or X1 = X7) and (X1 = a18 or a16 = X18 or X16 = a8) and X17 = X7 <=> a12 != X11 or X3 = a17 and X4 = a9 and a8 = a6 and X3 = X2 or a18 = X4 and X7 = a10 or a20 != X1 or a1 != X16 } |",
			"| { ( on X2, X3, X4, X10, X6, X7, X13, X20, X11, X18, X17, X16, X15, X9, X8, X19 ) ( X2, X3, X4, X10, X6, X7, X13, X20, X11, X18, X17, X16, X15, X9, X8, X19 ) | (X9 = X18 and a12 = a7 and a3 != X15 => a9 != X13 and a5 = a4 or X16 != a18 or a13 = a14) <=> ((X20 != X8 or a10 != a20) and a5 = X7 and X4 = X15 => a1 = a9 or X7 = a20 or X13 != X3 and a20 != X13) => (a8 = a16 or X19 = X8) and (a19 = a20 or X2 = a19 or a15 != X11) and (a12 = X8 or a11 = a14 or X6 != X16 or a7 = a1) and X3 != a18 and (a11 = X10 or X17 = X13) } |",
			"| { ( on X1, X2, X3, X4, X5, X6, X7, X14, X13, X12, X20, X11, X18, X15, X9, X8, X19 ) ( X1, X2, X3, X4, X5, X6, X7, X14, X13, X12, X20, X11, X18, X15, X9, X8, X19 ) | (a5 != X3 or a9 = X2 or a9 = a17 or a19 = X12 or a3 = X5 or a6 = a11 or a3 = a6) and (X11 = a7 or a20 = X12) and (a13 != a9 or a4 = a5 or a14 = X19 or a14 = X2 or a1 = a17) and X14 != X7 and (X5 != a20 or a16 = a17 or a20 = X8 or a4 = X14 or X5 = a19) and (a7 != a9 or a14 = X3 or a18 != X13 or X2 != a3 or a2 = X18 or a8 = a20 or a12 = X20) and (X9 != X3 or a17 != X19 or a11 != X2 or X15 = a11 or X1 = X4 or X6 != X1) and (a13 = X7 or true or X8 != a8 or a3 != X20 or a14 != a2) } |",
			"| { ( on X2, X4, X10, X5, X6, X7, X14, X13, X20, X11, X16, X15, X8 ) ( X2, X4, X10, X5, X6, X7, X14, X13, X20, X11, X16, X15, X8 ) | (X20 = X13 or a9 = a7 or a5 = X6 <=> X6 != a9 or X7 != a15 and a9 != X8 or a10 != X11 => true and a3 = X8 and a7 = a11 or X11 != a6 or X4 = a10 and a16 = a2 and X2 = a13 or a3 = X15 and a13 != X20 and a19 = a16) => X7 = X11 and X15 != a18 and X16 = X6 and X5 != a17 and a13 = a5 or a14 != a17 or a17 != X4 or X7 != X13 and a13 != a3 or a17 != X10 and a15 != a2 and a18 = X14 and X10 = a16 and a16 != a14 or a18 != X11 and X8 = X4 and X2 = a4 and X13 = a14 } |",
			"| { ( on X1, X2, X4, X10, X5, X6, X7, X14, X13, X20, X12, X18, X17, X16, X15, X9, X8, X19 ) ( X1, X2, X4, X10, X5, X6, X7, X14, X13, X20, X12, X18, X17, X16, X15, X9, X8, X19 ) | X16 = a11 and a15 = X20 and X13 = X4 or X18 = X7 or a20 != X15 and a3 = X18 and X1 != a3 or X16 = a11 and X4 != a17 and X14 != X2 or X4 = X10 and a10 != X6 and X19 != X12 and X14 = X13 and X17 != a8 or a6 = a4 and a18 = X2 and a6 = X5 and a15 = X9 and a1 != a8 <=> (X4 = X8 or a20 != a10 and a2 = X2 or a4 != a8 or X10 != a11 <=> (a19 != a16 or a15 = X20) and X7 != X13 and (a12 != a14 or a1 = X7) and (a14 = a16 or X14 != X19)) } |",
			"| { ( on X1, X3, X4, X10, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X9, X8 ) ( X1, X3, X4, X10, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X9, X8 ) | a8 = X5 and X6 = X5 or a15 != X10 and a19 != a7 and a19 != a10 and X3 = a17 or a17 = X8 and a10 != X7 or a2 = a4 and a13 = X14 and X9 != X11 and a5 = a1 and a8 != X18 and X20 != a4 or a6 = X14 and a6 != X17 and a12 != X13 and a13 != X18 or X8 != a20 and a16 = X1 and X16 != X1 and X18 != a19 and a14 != a11 and X1 = X11 or X17 != X16 and X13 = a19 and X4 != a20 and a2 = a5 or a4 = a6 and X12 != X13 and X4 != a16 and a15 = X14 and a11 = a8 and a20 = X12 and a19 != a6 } |",
			"| { ( on X1, X2, X3, X10, X4, X5, X6, X7, X14, X13, X20, X12, X17, X16, X15, X9, X8 ) ( X1, X2, X3, X10, X4, X5, X6, X7, X14, X13, X20, X12, X17, X16, X15, X9, X8 ) | ((a6 = X13 or X15 != a16) and a16 = X9 and (X7 = X16 or a9 != a6) <=> a7 != X14 and X12 = a16 or true and a16 = X9 or a12 = a17 and X17 != a20) <=> (X4 = a5 and X17 = X8 and (a13 != X12 or a7 = X13) <=> a17 != X10 and a3 = a18 or X5 = a6 and X6 != X14 or false and a15 != X6) => a18 != a7 and a1 = a12 or X3 != X12 and a11 != a10 and X1 != X4 and a12 = X17 and a18 = X9 or X7 = X20 and a1 != X15 or X20 != X15 and a10 = a11 and X5 = a2 and a10 != X16 and X3 = a5 or X13 = X14 or a8 = X2 and a10 = a2 } |",
			"| { ( on X1, X2, X3, X4, X10, X5, X6, X7, X14, X13, X12, X20, X18, X16, X15, X9, X8, X19 ) ( X1, X2, X3, X4, X10, X5, X6, X7, X14, X13, X12, X20, X18, X16, X15, X9, X8, X19 ) | a3 = a7 and X2 = X7 and X9 != a3 and X12 = X20 or a16 = X3 and a9 != a17 and X13 = X12 and a13 = X7 and X18 != X20 and a17 != X13 and a8 != a6 and X12 = X16 or a1 = a19 and a18 != X16 and a9 != a5 and X12 != X14 or X18 = X20 and X3 != X7 and X15 != a19 and X13 != a13 and a17 != a11 and a18 = X2 and a6 = a11 and X5 != a5 or X1 = a14 and X19 != X3 and X10 != X5 and X13 != X19 or a2 != a7 and X8 != a9 and X4 = a11 and a16 != X7 and X16 != X18 and X8 = X20 and a14 != a2 and X6 = X5 or a16 != a9 and X2 != a1 and a19 = X18 and X5 = a4 or a5 != X12 and X8 != X4 or X2 = a10 and a20 != a18 and a5 != a13 and X16 != a13 and a10 != a3 and a3 != X13 and X6 = X5 and a12 != X8 } |",
			"| { ( on X2, X3, X10, X4, X7, X14, X13, X12, X11, X18, X17, X16, X15, X8, X19 ) ( X2, X3, X10, X4, X7, X14, X13, X12, X11, X18, X17, X16, X15, X8, X19 ) | (X7 != a1 or a9 = X14 or X18 = a12 or a14 = X3 or a14 = a1 or a2 = X17) and (X8 != X18 or X15 = X11) and (X3 = a4 or a8 != X15 or X8 != a4 or X10 = X12) and (X18 = a6 or a7 = a3 or a7 != a11 or a1 = a10 or X12 = X8) and (X7 != a16 or a3 = a11) and (X12 != a18 or X4 = a14) and (X16 = X4 or a11 = a2 or a7 = a6 or a13 = X10 or X2 = X18) => (a18 = a15 and X10 != X17 and a14 = X4 or X19 = a9 and true and a2 = a7 or a4 != a19 and a15 != X16 and a20 != a18 or a17 != a13 => ((X10 != X7 or X19 != a5) and X7 != a1 and (X7 != X13 or a9 != a20) => X7 != X14 and X7 != X18 or X3 = a7 and X2 = a7 or a15 != a5 and a8 != a13)) } |",
			"| { ( on X1, X2, X3, X4, X5, X6, X7, X14, X20, X12, X11, X18, X17, X16, X15, X8 ) ( X1, X2, X3, X4, X5, X6, X7, X14, X20, X12, X11, X18, X17, X16, X15, X8 ) | X15 = a20 and X20 != X17 and a2 != X11 and true and X3 != a12 and a15 != a9 or X11 = X8 or X7 = a5 and X1 = a9 and X11 != a5 and X16 = a13 and X12 != a11 and a9 != a1 and X6 = X14 and X12 = X14 or X16 = a18 and X12 != a7 and X2 = X7 or a6 != a18 or a14 != X2 and X16 != X14 and X15 = X8 and X4 = a19 or X4 != X17 and a9 = a13 and a8 = a11 or X1 != a5 and a3 != X18 and a6 = X5 and X4 = a10 and X12 != a14 and X11 != a20 and X12 = a14 and X16 = X20 or X16 != X18 and a17 = X14 and a7 != a11 and X2 = X5 and X6 = a6 and a3 = a1 } |",
			"| { ( on X2, X5, X6, X7, X14, X13, X20, X12, X11, X18, X17, X16, X15, X9, X8 ) ( X2, X5, X6, X7, X14, X13, X20, X12, X11, X18, X17, X16, X15, X9, X8 ) | X15 = a4 or a12 = X14 and X18 != X6 and X15 = X8 and a18 = X17 and a9 = X17 and a17 = a19 or a8 != X18 and X15 = X7 and X8 != a10 and a5 != X8 and a7 = a8 or a13 != X16 and a18 != X18 and a8 != X14 and X9 != X5 and X13 = X12 and X8 != a18 and X15 != X7 or a8 != X13 and X8 = X16 and X11 = a14 and X12 = X13 and X8 = X12 or X18 != a10 or true and X13 = X17 and X15 = a3 and X16 != X9 and a1 = X9 and a18 = X6 and a13 = X8 and X6 = a3 or a3 != a2 or a1 = a2 and X17 != a18 and X20 != a9 and X2 = a6 and a17 != X2 and X16 != a13 } |",
			"| { ( on X1, X2, X3, X10, X5, X6, X7, X14, X13, X12, X11, X18, X17, X16, X15, X9, X8, X19 ) ( X1, X2, X3, X10, X5, X6, X7, X14, X13, X12, X11, X18, X17, X16, X15, X9, X8, X19 ) | X18 = a17 and (X13 = X1 or X5 = a11 or X7 = a12 or X13 != X5 or a7 != X12 or a5 != X7) and (X14 != a2 or X2 != X14 or a11 != a2 or X14 != a5) and (X3 = X1 or a3 = a8) and (a1 != X14 or a2 != X7 or a11 != a19) and (a18 != X19 or X18 != X19 or a7 = a13 or X3 = a7 or X18 = X8) and (X12 = a14 or X16 = a16 or true) <=> (X19 != a5 or a3 != X15 or a2 = X6) and (X13 = a12 or X18 = a17 or X19 != X15 or a6 = a14 or X8 != X19 or X5 = X13) and (X6 != X1 or X18 != X12 or X18 = a11) and (a2 != a16 or a7 = X12 or a4 = a8 or true or a18 != X3) and (a2 = X8 or X10 = X15 or a15 != X18 or X3 = X11) and (X14 = a12 or a12 = X9 or X2 != X17 or a1 = X12 or a14 != a12) and (X6 = a15 or a9 = X9 or a17 != a10 or a12 = X3 or X18 = X12 or a17 = X13) } |",
			"| { ( on X1, X2, X3, X4, X10, X5, X6, X7, X14, X13, X20, X12, X11, X18, X17, X16, X15, X9, X8, X19 ) ( X1, X2, X3, X4, X10, X5, X6, X7, X14, X13, X20, X12, X11, X18, X17, X16, X15, X9, X8, X19 ) | X19 = X1 and X9 = X1 and a17 != X2 and X13 = a15 and a19 != X12 or a9 != a18 and a19 = X12 or a15 != X17 and X1 != X8 and a8 != X15 or X13 != a10 and X1 = a11 and X15 != a14 and a7 != X17 and X7 = a18 and X4 = X10 and false or X2 != a11 and a15 = X9 or a2 != X14 or a20 = X12 and a3 != a20 and X13 = a1 and X11 != X16 and a16 = X7 and X4 != a12 and X18 = a20 and X8 = X17 and X5 = X17 or X6 != X5 and X12 != a17 and X9 != a3 and a2 = a8 and X8 != X10 and X7 != a7 and X13 != X4 or X20 != X5 and X6 = X11 or a18 = X8 and X13 != X14 and X3 = a11 } |",
			"| { ( on X1, X3, X4, X10, X5, X7, X14, X20, X12, X11, X18, X17, X16, X15, X9, X8, X19 ) ( X1, X3, X4, X10, X5, X7, X14, X20, X12, X11, X18, X17, X16, X15, X9, X8, X19 ) | (a14 = X16 or a16 = X14 or a15 = a14 or a20 != X8) and (a8 = a11 or a7 = X7 or a10 != a14 or a4 != X15 or a1 != X3) and (X1 = a15 or X9 = a11 or a4 = X12 or a1 != X10 or false or a3 = X20 or X9 != a10) and (a12 != X15 or a2 != a18 or X8 = a14 or a16 = X17 or a13 = X1 or a2 = X7 or a12 != a1 or X18 != a15) and (a2 = a12 or a20 != a5 or a10 != X8 or a20 = a16 or X20 = a7 or X4 != a14 or X14 = X18 or a14 = a9) and (X8 = X14 or true or X11 = a6 or a13 != X4) and (a2 != a3 or a15 != a20 or a8 = X4 or X1 != a14 or X17 = a10 or a11 = a16 or a10 = a4 or false) and (X7 != X18 or a13 != X7) and (a16 != X15 or a11 != X5 or X5 = a15 or X19 = a9 or X8 != X19 or a7 = a15) and (X18 != a19 or a11 = X19 or X8 = a14) } |",

			"| { ( on X3, X4, X10, X13, X12, X20, X11, X17, X19, X15 ) ( X3, X4, X10, X13, X12, X20, X11, X17, X19, X15 ) | a3 != a7 and X20 != X19 and a12 != a8 and a2 != X17 and X12 != X15 and X10 != a9 and a10 != a2 and X12 != a17 and a18 != X12 and X11 != a17 and a4 != X13 and a19 != X13 and a12 != a14 and a18 != X3 and a17 != X11 and X3 != a18 and X4 != a5 and a7 != X13 and a1 != a2 and a9 != a5 } |",
			"| { ( on X1, X2, X10, X7, X13, X12, X11, X8, X18, X19, X16, X15 ) ( X1, X2, X10, X7, X13, X12, X11, X8, X18, X19, X16, X15 ) | X1 != a18 and a12 != X16 and a10 != a8 and a9 != a2 and X12 != a3 and X2 != X8 and X10 != a7 and X18 != a18 and X13 != a4 and X11 != X12 and a13 != X15 and X13 != X7 and a17 != a1 and a4 != X1 and a19 != a14 and a9 != a17 and X12 != X10 and a19 != X15 and a19 != X11 and X16 != X1 and X1 != a11 and X18 != X2 and X10 != X19 } |",
			"| { ( on X2, X3, X4, X10, X5, X7, X14, X13, X12, X16, X15, X9, X8 ) ( X2, X3, X4, X10, X5, X7, X14, X13, X12, X16, X15, X9, X8 ) | a1 != X8 and X3 != a16 and false and a14 != X5 and X15 != a14 and a9 != a14 and a16 != a18 and X13 != X9 and X4 != a18 and a10 != a3 and X10 != X9 and a12 != a9 and a14 != a12 and a4 != a19 and a9 != X5 and a20 != X2 and X2 != a16 and X12 != X13 and X3 != X10 and X16 != X13 and a19 != X4 and X14 != a17 and a11 != a9 and X7 != a2 and X10 != X4 and X2 != a17 } |",
			"| { ( on X1, X2, X4, X10, X5, X6, X7, X14, X20, X12, X11, X18, X17, X16, X15, X9, X19 ) ( X1, X2, X4, X10, X5, X6, X7, X14, X20, X12, X11, X18, X17, X16, X15, X9, X19 ) | X16 != a16 and X11 != a12 and a18 != X4 and X4 != X16 and a17 != a5 and a20 != a17 and a5 != X12 and X1 != a10 and X10 != X7 and X9 != X14 and a6 != a5 and a1 != X17 and a4 != X1 and a13 != X12 and X2 != X19 and X2 != X18 and a4 != X19 and a4 != X12 and a5 != X1 and X5 != a12 and a6 != a7 and a6 != X11 and X9 != X20 and a7 != a10 and X7 != X6 and a7 != a2 and X7 != a20 and X19 != X17 and X6 != X15 } |",
			"| { ( on X1, X2, X10, X4, X5, X7, X14, X13, X11, X18, X17, X16, X8, X19 ) ( X1, X2, X10, X4, X5, X7, X14, X13, X11, X18, X17, X16, X8, X19 ) | X4 != X10 and X16 != a16 and a9 != X11 and X14 != X10 and a8 != X8 and X8 != a12 and X19 != X10 and X19 != X17 and X1 != a14 and a13 != a18 and a4 != a3 and X5 != a19 and X7 != X17 and a12 != X8 and X13 != a12 and a18 != a6 and a20 != X4 and X18 != a5 and a15 != a17 and false and a12 != a1 and X5 != a16 and X13 != X2 and a2 != X17 and a4 != X1 and a12 != a4 and false and a16 != a13 and a1 != a7 and X5 != a1 and a4 != a9 and X17 != X14 } |",
			"| { ( on X1, X2, X3, X10, X4, X5, X7, X14, X13, X20, X12, X11, X18, X16, X15, X9, X8, X19 ) ( X1, X2, X3, X10, X4, X5, X7, X14, X13, X20, X12, X11, X18, X16, X15, X9, X8, X19 ) | X10 != X14 and X20 != a13 and X16 != a12 and a17 != X19 and X18 != X15 and false and X19 != a4 and X13 != X4 and X12 != a10 and X12 != X3 and a9 != X16 and X5 != a11 and X9 != X20 and a17 != a1 and X1 != a8 and a11 != a14 and a18 != a7 and a18 != a9 and X13 != a7 and X11 != a7 and X5 != a16 and X4 != X12 and a1 != X7 and a7 != a16 and X2 != a3 and X7 != X8 and a7 != X4 and a13 != a15 and a4 != a2 and X16 != a16 and X4 != X20 and X5 != a19 and a17 != a12 and a14 != a9 and X12 != X10 } |",
			"| { ( on X1, X10, X4, X5, X6, X7, X14, X13, X20, X11, X18, X17, X15, X9, X8, X19 ) ( X1, X10, X4, X5, X6, X7, X14, X13, X20, X11, X18, X17, X15, X9, X8, X19 ) | X9 != a17 and a10 != a6 and a18 != a19 and a10 != X10 and a14 != X20 and a19 != X8 and a10 != a6 and X4 != X14 and a14 != X10 and a18 != a19 and a17 != a12 and a4 != X5 and X13 != a12 and a8 != a11 and X18 != X15 and X10 != X7 and X4 != a3 and X11 != a8 and X20 != a4 and a1 != X5 and X19 != X9 and X7 != a3 and a7 != X4 and a13 != X7 and a8 != a4 and a3 != a5 and a13 != a18 and X4 != X9 and X5 != X1 and X6 != a19 and a5 != X17 and a16 != a12 and X1 != a19 and a17 != X11 and X20 != a9 and X6 != X15 and a11 != a5 and X20 != X5 } |",
			"| { ( on X1, X4, X10, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X15, X9, X8, X19 ) ( X1, X4, X10, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X15, X9, X8, X19 ) | X12 != X8 and X4 != X18 and a6 != a9 and a14 != X10 and a4 != a18 and a11 != a16 and a12 != a1 and a18 != X5 and X6 != a6 and a5 != X1 and X10 != a18 and a7 != X15 and a9 != a14 and a17 != X16 and X12 != X4 and X6 != X5 and X16 != a1 and X11 != X4 and a17 != X20 and a5 != a17 and a9 != X6 and a19 != X7 and a11 != a2 and X7 != a4 and X13 != X10 and X18 != X14 and X14 != X15 and X16 != a11 and a3 != X7 and a5 != a13 and a14 != X1 and X7 != a5 and X12 != a9 and X19 != X17 and a15 != X8 and a7 != a16 and a5 != X10 and X9 != a1 and a18 != a6 and X9 != a3 and X19 != a6 } |",
			"| { ( on X1, X2, X4, X10, X5, X6, X7, X14, X13, X12, X20, X11, X17, X16, X15, X9, X8 ) ( X1, X2, X4, X10, X5, X6, X7, X14, X13, X12, X20, X11, X17, X16, X15, X9, X8 ) | a1 != a8 and a11 != X1 and X2 != a6 and X14 != a17 and a15 != a14 and a14 != X4 and X10 != X17 and a11 != X11 and a5 != X9 and X8 != a4 and a18 != a15 and X11 != a8 and X15 != a7 and X15 != a4 and a19 != a16 and X1 != X11 and a9 != X9 and a20 != a1 and X13 != X4 and a14 != a6 and a18 != a17 and X8 != X13 and X2 != a9 and X7 != X20 and a1 != X9 and a10 != a17 and X17 != X12 and a4 != a20 and a15 != X12 and a14 != X16 and a11 != a2 and a6 != X16 and X16 != X11 and X8 != X15 and X20 != a8 and X20 != X13 and false and X8 != a1 and X6 != X15 and X14 != X5 and a14 != a2 and a6 != a7 and a5 != X4 and X16 != a11 } |",
			"| { ( on X2, X3, X10, X4, X6, X14, X13, X12, X20, X11, X18, X16, X15, X9, X8, X19 ) ( X2, X3, X10, X4, X6, X14, X13, X12, X20, X11, X18, X16, X15, X9, X8, X19 ) | a20 != a2 and X12 != X14 and a16 != a2 and a19 != X2 and X16 != X19 and a16 != a9 and a14 != a5 and X18 != X19 and X13 != X2 and a8 != X15 and X18 != a6 and X19 != X10 and a14 != a17 and a8 != a6 and X2 != X8 and a9 != a12 and a1 != a16 and a13 != a6 and a4 != X11 and X16 != a18 and X12 != a9 and X14 != a12 and a7 != a2 and X4 != a20 and a20 != a18 and X13 != X20 and X16 != a18 and a5 != a16 and a17 != a5 and a20 != a4 and a16 != X19 and X13 != a4 and X9 != a15 and X6 != a17 and a15 != X8 and a8 != X6 and a3 != X14 and a15 != X10 and X6 != a8 and a9 != a18 and X14 != a6 and X15 != X3 and a3 != a6 and a1 != a13 and a16 != X4 and X19 != a4 and a4 != X20 } |",
			"| { ( on X1, X2, X3, X10, X4, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X15, X9, X19 ) ( X1, X2, X3, X10, X4, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X15, X9, X19 ) | X13 != a14 and X6 != a20 and a6 != X17 and X6 != X16 and a1 != a9 and X1 != a6 and a3 != a2 and a20 != X6 and a4 != X17 and a3 != X12 and X20 != a18 and a18 != X14 and X20 != X4 and a15 != X12 and X3 != X4 and a19 != X18 and X7 != X9 and X12 != a13 and false and X19 != a4 and X18 != a19 and a10 != a12 and X3 != a2 and X12 != a17 and a8 != X1 and a5 != a10 and X16 != X20 and a12 != X1 and a19 != a5 and a10 != a8 and a7 != X16 and X15 != X19 and X18 != X15 and X17 != a11 and X13 != a16 and X11 != X17 and a14 != X13 and a3 != X7 and a9 != a7 and a10 != X16 and X9 != X12 and X2 != X15 and a10 != X20 and X1 != X5 and a13 != X10 and a14 != a1 and X18 != X16 and a1 != a3 and X11 != a7 and X18 != a19 } |",
			"| { ( on X1, X2, X3, X4, X10, X5, X6, X7, X14, X13, X20, X12, X11, X18, X17, X16, X15, X9, X8 ) ( X1, X2, X3, X4, X10, X5, X6, X7, X14, X13, X20, X12, X11, X18, X17, X16, X15, X9, X8 ) | X9 != X17 and X18 != X14 and X11 != a5 and false and a19 != X18 and a4 != X9 and X20 != X8 and X12 != a12 and X1 != a3 and a8 != X14 and X11 != a3 and a4 != a11 and a5 != a10 and X10 != a16 and X2 != a15 and false and a2 != X10 and a1 != a13 and X1 != a3 and X2 != a15 and X17 != a5 and a7 != a20 and a5 != a4 and a19 != a8 and X15 != X11 and X11 != X2 and a13 != a2 and a3 != a8 and a2 != X12 and X3 != X16 and X13 != a13 and a18 != a11 and X20 != a17 and a7 != a3 and X4 != a18 and X14 != X1 and a6 != a18 and a8 != X12 and X15 != X2 and a18 != X4 and X20 != X5 and X6 != X10 and a19 != a14 and X9 != a5 and a14 != X11 and X14 != a16 and a3 != a4 and a8 != X7 and a19 != a13 and a12 != X15 and X15 != a16 and a7 != X6 and a18 != a2 } |",
			//"| { ( on X1, X2, X3, X10, X4, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X15, X9, X8, X19 ) ( X1, X2, X3, X10, X4, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X15, X9, X8, X19 ) | a10 != a5 and a2 != X6 and a8 != X19 and a1 != X6 and false and X2 != a12 and X12 != a15 and X12 != X4 and X7 != X5 and X12 != X6 and X3 != X20 and a2 != X16 and X4 != X20 and X12 != X4 and X16 != X11 and a2 != a10 and a9 != a16 and X7 != a3 and a4 != X15 and X8 != X16 and a4 != a16 and a7 != a10 and X5 != a16 and X8 != X5 and false and X20 != X15 and a18 != X4 and a18 != a4 and a12 != a15 and X10 != X9 and X9 != a13 and a7 != a3 and a1 != a5 and a10 != a9 and a10 != X1 and a6 != X20 and a18 != X13 and false and a13 != X1 and X6 != X14 and X16 != X12 and X18 != a7 and X18 != a14 and a17 != X2 and X1 != a17 and a6 != a4 and X18 != X6 and X20 != X19 and X5 != X20 and X14 != a8 and X3 != a14 and X9 != a15 and X3 != X9 and X15 != a14 and a15 != X17 and false } |",
			//"| { ( on X1, X2, X3, X10, X4, X5, X6, X14, X13, X12, X18, X17, X16, X15, X9, X8, X19 ) ( X1, X2, X3, X10, X4, X5, X6, X14, X13, X12, X18, X17, X16, X15, X9, X8, X19 ) | X15 != a14 and a4 != a11 and X16 != a19 and a18 != X6 and a11 != a1 and a18 != X13 and X8 != X5 and a7 != a2 and X1 != a2 and a8 != a15 and a2 != X5 and a12 != X10 and a1 != a5 and X14 != X4 and X9 != X16 and a4 != X14 and X14 != X13 and a1 != a4 and a19 != a12 and X17 != a20 and X6 != a17 and a7 != a17 and a13 != a17 and X1 != a2 and X5 != a12 and X13 != X6 and a10 != a8 and a17 != a20 and X10 != a6 and a14 != a4 and a1 != X14 and a3 != a16 and a13 != X10 and a20 != X2 and X18 != a8 and X3 != a2 and X1 != a7 and X18 != a13 and a8 != a4 and a19 != X14 and X19 != X3 and a2 != a18 and a9 != X17 and a9 != X1 and X16 != a14 and a16 != X1 and a16 != X14 and X18 != X4 and X13 != a5 and X12 != X9 and a11 != a4 and a11 != X4 and X1 != X6 and a1 != a13 and a5 != X8 and a11 != a12 and X2 != a3 and a3 != X16 and a19 != X17 } |",

			"| { ( on X1, X2, X3, X4, X10, X5, X6, X7, X14, X13, X20, X12, X11, X18, X17, X16, X15, X9, X8, X19 ) ( X1, X2, X3, X4, X10, X5, X6, X7, X14, X13, X20, X12, X11, X18, X17, X16, X15, X9, X8, X19 ) | (X12 != a18 or X19 = a1 or X20 = X8 or a13 != a15 or X7 = a6 or a1 = X5 or X20 = a18 or X13 = a12 or a14 = X15 or a20 = X14) and (X8 = a11 or X17 != X16 or a11 != X7) and (a1 = X4 or a9 != X7 or X7 != X3 or a16 != X1 or a15 = X2 or a2 != X7 or X4 = a2 or a1 = X16 or X5 = X11 or X16 = a13 or X5 = X2 or a1 != X10 or X10 = a8 or X5 = X4 or a8 != a4 or X8 = X19 or true or X17 != X5 or X17 != X8) and (a15 != a1 or a1 = a15 or X13 = a18 or a1 = a19 or a14 != X6 or a6 = a20 or X15 = X18 or a16 != X12 or X8 = a1 or X20 != X5 or a14 != X13 or X5 != X6 or a7 != X17 or a11 = a20 or a7 != a5 or X13 != X1 or a16 = X3 or X2 != a7 or X16 = a17 or X10 != X9 or false or a15 = X6 or X16 = a20 or a10 = a12 or X14 = X9 or a17 = X7 or a8 = X20 or X6 != a18 or X20 != a16 or X9 = X18 or a11 = X7 or a1 != X8 or X20 = X13 or X18 != X6 or a4 = a19 or X20 != a5 or a15 = a5 or X10 = a15 or X6 = X20) and (X10 != a13 or a8 != X18 or X14 = a9 or X2 != X12 or X6 != X2 or a6 != X20 or X16 = a5 or X6 != a2 or X5 != X1 or X20 != a2 or a12 != a7 or X13 != a5 or X1 = a4 or X18 = a19 or a5 = a20 or a18 != X12) and (a1 != X7 or X15 = X3 or a9 != a11 or a4 != a15 or X20 != a18 or X6 != a20 or a1 != X6 or X7 != a20 or a7 != X6 or a14 != a13 or a1 = X7 or a13 = X5) and (X13 = X12 or a18 = X19 or X7 != X16 or X17 = a20 or X4 != a4 or X4 = a5 or a2 = a12 or a10 != a16 or X5 != X12 or a18 = X13 or a13 = X11 or a16 != X18 or X7 != X6 or a1 = a6 or a18 != X10 or X12 != a10 or X20 != a11 or a16 = X14 or a4 = a8) and (a5 = a3 or a9 != X10 or X17 = a1 or X4 = a17 or X11 = a2 or X18 != a8 or a14 = X14 or a13 != a11 or X9 != a1 or X9 != X19 or X9 != X15 or X15 = X6 or X1 = X6 or X20 != a12 or X20 = a2 or X3 = X5 or a15 != X5 or a8 = a13 or a19 = a8 or a17 != X11 or X4 = X12 or a1 != X13 or a6 != a20 or X4 = X20 or a20 != X1 or X3 != a17 or X13 = X6 or a18 != X15 or a9 != X15 or X9 != a12 or a15 = a19 or X19 != X18 or X1 != X18 or X6 != a16 or a11 = a12) and (X12 = a2 or X2 != a11 or X19 = X14 or a7 != a15 or X3 = a18 or true or X10 != X8 or a19 != a7 or a18 != a7 or a2 = a7 or a19 = a4 or a15 != X17 or X14 != X5 or X16 != X12 or X2 = X20 or X8 != a17 or a19 != a6 or X1 = a9 or a9 = a17 or a12 != X3 or X8 = a15 or a2 = a15 or a6 != a1 or X7 = X12 or a20 = a12 or X11 = a16 or a6 != X13 or X8 != X18 or X15 != X18 or X11 = X6 or X20 != a19 or a8 = X15 or a3 = X2 or a11 = a18 or a20 = X18 or a17 = X20 or X8 != a9 or X5 != a7 or a19 != X8 or X17 = a20 or a6 = a12 or X14 = X13) and (X17 = a12 or X18 = X14 or a16 = a12) and (a2 != a3 or a15 != a2 or X5 != a12 or a1 = X13 or X19 = a20 or a14 != a9 or a13 = X20 or X20 != a7 or X10 = a9 or X5 = X18 or false or X16 = X18 or X1 = X19 or a4 != a9 or a4 != a15 or a17 != a2) and (X15 != X20 or X10 = X8 or X6 = X1 or X17 = X13) and (X13 = X11 or a5 = a2 or X4 = a7 or X3 != a7 or X5 != X14 or X4 != X18) and (X4 = a19 or a16 = a17 or a20 = a7 or a1 = a6 or a17 = a4 or a3 != a15 or a1 = a19 or a9 = a2 or X3 != a13 or X10 != a12 or a12 != a4 or X20 = a14 or X13 != a13 or X13 != a8 or a7 = a16 or X2 = X19 or a3 = X6 or a17 != a16 or X20 != a15 or X7 = X1 or X19 != X11 or X2 != X9 or a19 != X13 or a19 != a7 or a19 = X14 or a11 = X6 or X2 != a5 or X15 = a3 or X3 != X20 or X16 != a4 or X18 != a18 or a15 != X3) and (a9 != X17 or X10 = X7 or X5 = a4) and (true or X14 = X2 or X14 != X11 or X13 = X7 or X1 != X17 or X2 = X13) and (X12 = a10 or a3 != X9 or a12 = a6 or X20 = a15 or X20 != a11 or X17 = X6 or a11 = a6 or a12 = X14 or X15 = X8 or X14 = X12 or X20 != a2 or a13 != a10 or X1 = X15 or X2 = X19 or X18 = X14 or a11 != a2 or false or X7 = X8 or X19 = a2 or false or a7 != a15 or a8 = a7 or X6 = X3 or X15 = X2 or a10 = X11 or a11 != X16 or X13 = a1) and (X18 = X8 or a19 != X20 or X11 != a9 or a20 != X19 or a17 != X12 or a6 != a13 or a8 = X10 or X10 = X17 or X12 = a7 or a14 = X19 or X4 != a19 or a2 != a20 or X6 != a11 or a10 = a9 or a1 != a18 or a15 != X16 or X20 = X15 or a12 = X17 or a12 != a17 or a15 = a17 or a9 = X3 or a10 = a15 or a3 = a16 or a10 != X7 or a18 != X2 or X15 = a13 or X6 = a5 or a6 = X12 or X13 != a7 or a20 != X3 or a4 != a14 or X3 = X6 or X16 = X19 or X2 = a2 or a20 = a6 or X6 = a16 or X18 != a3 or X17 = a15 or a16 = X12 or X2 != X1 or X14 != a7 or false or true) and (a10 = a6 or X7 = a18 or X5 != X7 or X20 != a10 or a14 != X2 or a15 != X10 or a9 = a5 or a12 = a10 or X16 != a13 or X12 = X14 or X17 = a20 or a6 != X9 or a17 = X16 or X10 != X4 or a9 = a13 or X2 = a15 or a9 != a7) and (a6 = a7 or X11 = X18 or X6 = X7 or a14 = a9 or X2 = X15 or a14 != a6 or X9 != X3 or a5 = X15 or a10 != a13 or X6 = a18 or X3 = X5 or a20 = X4 or X15 = a19 or a6 != X12 or X18 = X5 or a11 = X8 or a16 = a8 or X1 = X11) and (X14 = X6 or X8 = X15 or X4 != X9 or a19 = a10 or X20 = a3 or a9 != a8 or a19 != a20 or a2 != X4) and (X4 != X13 or a3 = X3 or X3 = a13 or X7 != X12 or X16 = X8 or X9 != X19 or a4 != X8 or a13 != a14 or a3 != X8 or a11 = X9 or a17 = X16 or X19 != X7 or X7 != a13 or X9 != a4 or false or X14 != X15 or X3 = X19 or a14 != X6 or a6 = a19 or X3 != X12 or X19 != a17 or a9 = X12 or a2 = a11 or X7 = a8 or X9 != a2 or X13 = a19 or a14 != X12 or X10 != a4 or X19 != X2 or a9 != a18 or X5 != a14 or a4 != X2 or a10 = a18 or X1 != a7 or a11 = X1 or X13 = X20 or X16 != X5 or a16 != X5 or a4 != X16) and (a9 != a15 or a9 != X5 or a6 = a17 or a11 != a17 or X4 = X17 or X5 != X7) and (a13 != a20 or X12 = X15 or false or a17 = X17 or X13 = a10 or a11 != a19 or a13 = a1 or a19 = X18 or X1 != X19 or a3 = X19 or X10 != X15) and (X2 = a6 or X3 != a7 or X1 = X8 or a8 = a5 or a9 != a3 or a15 = X19 or a20 = X6 or a1 = X18 or a18 != X5 or X15 != a6 or a3 = a13 or X6 != a20 or X5 != a6 or a14 != X11 or a16 != X16 or a16 != X1 or X17 != X10 or a11 != X16) and (a7 = a12 or a12 = a1 or a10 != X2 or a14 != X4 or a4 != a19 or X15 = a7 or a10 = a4 or X7 = X17 or a18 != a20 or X1 != X18 or X7 != X20 or a12 = X8 or X12 = a19 or X5 != X3 or a16 != X15 or X5 = X15 or X9 != a11 or a11 = X12 or X17 != a8 or a11 != a10 or a2 != X13 or X9 != a15 or X18 = a13 or X20 != a5 or a9 = X13 or a16 != a9 or X15 = a11 or a17 = X2 or a3 = a5 or a10 != X15 or X20 != a13 or a13 != X19 or a10 = X4 or X10 != a19 or X11 != X2 or a7 = a12 or a3 = X18 or a9 = X8 or X1 != a9) and (X17 != a6 or a12 != a5 or a10 = X5 or X3 = a20) and (a11 = a4 or a6 != a15 or a17 != a20 or X12 = a9 or a15 = a18 or X18 != a8 or X7 = X11 or X9 = a11 or a13 = X12 or a13 != X14 or a1 = X14 or X8 != X10 or X9 = a3 or X10 = a1) and (a18 = a11 or a1 != X10 or X8 != a13 or X9 = a16 or X18 != a20 or a5 = a14 or a2 = a9 or false or a9 = X15 or a19 != a13 or X15 != X19 or X11 != X2 or a16 != a7 or X7 = X9 or a17 = X19 or X5 = a12 or X17 = X9 or a12 = X17 or X2 = X17 or X18 = X16 or X10 = a19 or a1 != X14 or a2 != a10 or X7 != X2 or X20 != a19 or a17 = a10 or X11 != a16 or a7 = X12 or X17 != a18 or a3 = X7 or a14 != a7 or X2 = a20 or X7 != X8 or X15 = a14) and (a20 = a13 or X18 != a15 or X6 = X10 or X6 = X8 or X17 != X5 or X8 != X4 or X5 = X6 or X2 != a10 or a11 != a1 or X12 = a10 or X16 != X10 or X17 = X16 or X6 != a9 or a11 = a2 or a13 = a16 or a1 != a4 or a5 = X16 or X17 = X15 or X4 = X3 or X20 = a3 or a13 = a14 or X8 != X11 or X4 = X17 or X3 != a10 or a9 != a6 or a13 != X13 or X1 != a15 or a1 != X19 or X20 != a3 or X9 = a7 or X6 != X10 or a17 != a18 or a7 != X3 or a8 != a12 or X14 != a2 or X19 != a9 or X7 = X6 or true) and (X19 = X10 or X8 = a3 or X13 != a4 or a13 != a14 or X20 != a2 or X18 = X1 or a5 = X9 or a6 = X7 or X12 = X17 or a11 != a13 or X7 = a18 or X20 = X3 or X10 = a16 or X4 != X1 or X6 = a8 or a11 = X9 or X3 = a17 or X19 = X3 or X8 != a6 or X8 = a3 or X6 != X3 or a10 != X15 or a18 != X15 or X12 = a17 or X18 != a12 or a9 != X1 or a8 != a11 or X2 != a14 or true or a11 = a5 or a5 = X10 or a1 != a11 or a7 != X9 or true or X19 = a14 or a3 != a8) and (a15 != a8 or a12 = X14 or a12 = a16 or a13 != a9 or a20 = X13 or X17 != X5 or X6 != X11 or X15 = X1 or X5 = a11 or X9 = X1 or X16 = a5 or a11 != X17 or a11 = X4 or a1 != a12 or a1 = X17) and (a7 != X4 or a16 != a2 or X9 = a9 or X19 != X4 or X18 = X5 or X10 != a10 or a4 = X8 or X20 = a19) and (a10 = a7 or a14 = X9 or X6 = a4 or X12 != a7 or X14 = a20 or X11 != X15) and (X2 != X3 or X15 != X19 or X7 = a10 or X13 = a1 or X7 = X16 or a3 = a9 or a7 = a11 or a5 != X7 or a5 != X5 or a15 != X18) and (a5 != X10 or a17 = a5 or a17 = X17 or X19 != X6 or X2 != X14 or X20 = a6) and (a15 = a16 or a11 != X6 or X9 != a18 or a5 = a15 or X2 = a9 or X19 != a9 or a12 != X1 or X8 != X12 or X11 = a5 or a11 != a17 or X5 != a16 or a17 != X8 or X18 = a6 or X13 = X16 or X20 != X7 or a5 != a4 or a7 != X14 or X12 != X4 or a17 != X17 or X15 = a2 or X5 = a16 or a14 != a4 or X5 = X16 or a18 != X5 or X16 = X5 or a15 != a13 or X3 != a7 or X13 = a3 or a19 != a10 or X15 = a19 or X3 = X7 or a19 != X11 or X18 = a19) and (X7 != a2 or X11 != a4 or a15 = a4 or X20 = a10 or a2 != X15 or X15 != X11 or a1 = a19 or a16 != X10 or X16 != X6 or X8 = a11 or a7 != a6 or X1 != X20 or X19 = X12 or X6 = X16 or a6 = X12 or a12 != X2 or X14 = X17 or a15 = X20 or a6 = X2 or X10 = a17 or a14 != a5 or a1 = X3 or X9 = X7 or X16 != a5 or a3 = X4 or a16 = a4 or a16 = a10 or a5 != a12 or a8 = X16 or a12 = X12 or a11 != a16 or X20 = X8 or X6 = X12 or X18 != X14 or a9 = X16 or X20 != a1 or X20 != X3) and (X17 = a20 or X13 != a19 or X11 = a20 or a1 != X4 or X20 != a17 or X5 = a1 or a5 != X13) and (a3 != a4 or a4 != a12 or a16 != X12 or a2 != a17 or X7 != a12 or X14 = a19 or X13 != X17 or X17 = X1 or false) and (X5 != X18 or X10 = a7 or a15 = a2 or X15 != a10 or X1 = X18 or a9 != a12 or a6 != a10 or X3 = a18 or false or X1 = X8 or X6 = a19 or a8 = X6 or a6 != a13 or a6 = X18 or X4 = a16 or a5 != X7 or a8 = a4 or X9 != X3 or X1 != X3 or a9 = a6 or X11 != a16 or a13 != a17 or a8 = X14 or X5 != a2 or X20 = X14) and (X12 = a4 or X7 != a13 or a11 != a18 or X2 != X18 or X12 = a11 or a9 = X5 or X9 = X8 or a18 != a17 or a10 != X4 or a16 = a8 or a16 = a14 or X19 = X8 or a17 = a15 or a13 != X17 or X9 != X12 or X9 = X7 or X12 != a10 or X18 = X16 or X9 = a18 or X3 != a3 or false or X7 != X11 or a9 != a1) and (X12 = X18 or a9 = a5 or X18 != X17 or a10 = a19 or a1 != a4 or a12 != X12 or X13 != X2 or a6 = X17 or a2 = X4 or a19 = X9 or X5 = X7 or a3 = X17 or a3 = X15 or X10 != a19 or true or X14 != X1 or X11 = X18 or a3 = a18 or a3 = X19 or X17 = a8) and (a20 = a4 or X8 != X7 or a2 != X20 or a10 != X11 or X3 = X4 or X8 = X18 or a1 = X11 or a9 != X3 or a14 != X19 or X16 = a9 or X13 = a3 or X7 = X9 or a4 = X6) and (X4 != X19 or a1 != a12 or a7 != X12 or X14 = a2 or a12 = X1 or a6 != X17 or a12 = a8 or a20 != X6 or false or a8 = X10 or X11 = X1 or X12 = a3 or a5 != X16 or a20 != X12 or X18 != a8 or X4 = a2 or a2 != a16 or a18 != a12 or a9 = X16 or a16 = X6 or a10 = a1 or a7 != a12 or a14 = X3 or a18 = X14 or a13 != a5 or X2 = a13 or X8 = a20 or X4 = a12 or a7 = a17 or a20 != X6 or a12 = a3 or a2 != a14 or false or X12 = X16 or X3 != a16 or X10 != a14 or X16 != a16 or a10 != X8) } |",
			"| { ( on X1, X2, X3, X4, X10, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X15, X9, X8, X19 ) ( X1, X2, X3, X4, X10, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X15, X9, X8, X19 ) | (a2 != X14 or X6 != a8 or X14 = X4 or X14 != X18 or X19 != a3 or X18 != a2 or X10 != a16 or a12 != X5 or X19 = X7 or a2 = a11 or a7 != X2 or a10 != a12 or X12 != X14 or X18 != X12 or a12 != X14 or a9 = X10 or X20 = a8 or a19 = X12 or a14 = a1 or a1 = X2 or a6 = a19 or a15 != X1 or a6 != X3 or a16 != X19 or X20 != X8 or a2 != a5 or X5 = X14 or X17 != X10 or X14 != a17 or a12 = X18 or a19 = X3 or X8 != X4 or X20 = a13) and (X9 = a6 or X13 != a7 or X5 != X12 or X15 = X20 or X20 != X19 or X8 != a12 or a8 != a11 or a9 = a16 or X11 != X14 or a5 != a4 or a11 = a2 or false or a12 != a14 or X14 != a18 or a2 = a14 or a20 != a17 or X4 != a1 or X10 = X14 or a10 != a12 or X9 != a12 or a19 = a15 or X11 != X3 or a20 != a14 or X16 = X6 or a13 != a1 or X2 != X11 or X2 != X7 or X17 != X3 or X2 != X15 or X16 = X5 or X6 != X7 or X5 != X3 or a4 = X8 or X16 = a18 or a17 = a1 or a11 = a3 or a9 = X15 or a17 = X10 or a17 = X7 or X20 = X7 or X2 != X1 or a11 = a14 or a15 != X18 or a10 != X4) and (X7 = X6 or a16 = a12 or X8 != X13 or true or X17 = a7 or a15 = X4 or a4 = a5 or X19 = a7 or X12 != X19 or a14 = X1 or a19 != X5 or false or a2 = X5 or a15 != a18 or X3 != X13 or X1 = a4 or X7 != a20 or X2 != a16 or X10 != a12 or a7 != X5 or a9 = X18 or a6 = a3 or a19 = X14 or X6 != X3 or X2 = a20 or a3 != a16 or a20 = X14 or a6 != X3 or a13 = a12 or a19 = X5 or X12 != a5 or a20 != X2 or X4 != a9 or a14 != X20 or X16 != a13 or a9 != X17 or X19 != X20 or a16 = a14 or X11 != a14 or X20 != a13 or a1 = a12 or X19 = a7 or X15 != X19 or X12 != X4 or a17 != X17 or X9 != a20 or X11 != a1 or a9 != a8) and (X6 = X18 or X13 != a6 or X8 = a18 or a10 = a8 or false or X8 = a9 or X17 = a8 or a2 != X13 or X20 != X9 or X17 = a19 or a4 != a19 or a3 != a6 or X7 = a10 or X3 != X4 or a20 != X18 or a20 = X5 or a20 != a14 or X19 != X5) and (X16 != X13 or a6 != a17 or a11 = X1 or X16 != a3 or X19 != a19 or X15 = a10 or false or X16 = a13 or a18 = X4 or a14 != X4 or X17 != a4 or X4 != X20 or a7 = X2 or a20 = a8 or a20 != X12 or a18 = X9 or X12 = X11 or X15 = X6 or a4 != X13 or X6 != X4 or X16 != a12 or a9 = a6 or a6 = X17 or X15 = X2 or X17 = a15 or X13 != a1 or a8 != X15 or X10 != a3 or X9 = a18 or a20 != X16 or X14 = a9 or a17 != a9 or false or a8 != X12 or X1 = X15 or X15 = X10) and (a3 = a15 or a3 = X20 or a4 = X8 or X14 = X16 or X20 = a18 or X15 != a3 or a12 = a20 or X19 = X1) and (X11 = a15 or a20 != X7 or X15 = a18 or X9 = a19 or X3 != X15 or X10 != X4 or a3 != X18 or X18 = a14 or a10 != X1 or X3 != X7 or a12 = a8 or a3 != X7 or X2 = X7 or a11 != a14 or a3 = X2 or X3 = a18 or X13 = X2 or X12 = X17 or X20 = a16 or X18 = X1 or a13 != X4 or a8 = a1 or a16 != a15 or a17 != X7 or X4 = a8 or a1 != X19 or a20 != X8 or X20 != a1 or X4 = X11 or X4 = a1 or a11 != a1 or X20 = a18 or X2 != a10 or X6 = X14 or a17 = a6 or a2 != a18 or X18 = X10 or X18 = a4 or a11 = a4) and (false or a12 != X7 or X4 = a3 or false or X14 != a14 or a7 = a20 or a5 = X16 or X11 = X15 or a8 != X4 or X19 = X20 or a2 != X4 or a5 = X9 or a17 != a13) and (a2 = X11 or X13 != a10 or a18 = X9 or a11 != a4 or a17 != a15) and (a20 = a2 or X9 = X15 or X9 = X8 or X9 = a2 or a15 = X12 or a18 != X3 or a19 != X1 or X11 != X5 or a11 = a9) and (X7 != X17 or a19 != a2 or X7 = a16 or a2 != a1 or X14 != a15 or X11 != a9 or a20 != X16 or X12 != X14 or a18 = a13 or a13 = X4 or a5 = X7 or X18 != X16 or X17 != a13 or X14 != a6 or a9 = X8 or a3 = a2 or a19 = a18 or X4 = a19 or a3 = X2 or X13 = a10 or true or a1 != X19 or a14 != a9 or false or a14 = a11 or a17 != a4 or a3 = a8 or X6 != X18 or X5 = X6 or false or X3 != a2 or X12 != a13 or X7 != X2 or a20 != X7 or X4 != a13 or a13 = a3 or X10 = a15 or X3 = a4) and (a2 = a18 or X9 = a15 or a8 != X7 or X8 = a16 or X4 != a12 or X9 = a8 or X2 = X3 or a14 = X20 or a19 = X6 or X4 = X14 or X17 = X15 or a8 != a3 or a17 = a7 or X15 = X2 or X19 != X9 or X2 = a15 or a13 = X1 or X2 != X20 or X12 = a12 or a18 = X17 or a14 = X9) and (X8 != X16 or a15 != X10 or a2 = X7 or X19 != a16 or a6 != a4 or X7 != X12 or a4 = a3 or a3 != a8 or X18 = X17 or a2 != a6 or a13 != a5 or X18 != X1 or a16 = a9 or X20 != X7 or X13 = X14 or X3 != X9 or a7 != X17 or a1 != a3 or X14 != a13 or X4 = a3 or X19 != a12 or X7 = a2 or X17 = a14 or a4 != X7) and (a6 != X6 or X11 != a14 or a11 = a13 or a1 != a5 or a20 = X2 or X5 = X16 or a3 = X20 or a20 = X19 or X1 = a15 or a4 != a13 or X3 = X16 or X4 = X7 or X19 = X3 or X9 != a6 or a15 = X19 or a15 = X19 or X6 != a6 or a6 != a9 or X13 != X9 or a3 != X19 or a10 != a14 or X5 = X15 or X15 = a19 or X18 != a3 or X13 = a15 or a11 != X18 or X17 != a19 or true or a3 != a1) and (X19 = a18 or a19 != X6 or X11 = a11 or X18 = a9 or a11 != a9 or X17 != X5 or X11 = X18 or a20 != X13 or X1 = a4 or a18 = X2 or a8 != a11 or X2 = X11 or X15 = X4 or X19 = a17 or X4 != X3 or a4 = X12 or X11 != X17 or a10 = a14 or X12 = X13 or X9 != X19 or a9 != a19 or X4 = a11 or X12 = a7) and (a4 != X19 or a8 = X17 or a6 != a15 or a3 = X12 or X5 = X4 or X6 = a5 or X18 != a4 or X11 = a11 or a3 != X8 or X3 = X15 or a3 = X6 or a10 != X3 or X17 != X20 or a15 = a4 or X3 != X15 or a5 != a6 or a5 != X1 or X6 = X13 or a6 = X10 or a18 = X9 or a14 != X5 or X18 = a14 or X13 != a8 or a13 = a18 or X13 != a5 or X18 = a2 or a1 = a5 or X10 = a9 or a17 != X14 or a5 = a6 or X4 != a11 or a20 != X15 or X6 = a6 or X17 = a15 or a7 != a18 or X6 != X7 or X14 != a12 or a5 != X14 or X11 != X19 or a11 = a12 or false or X14 != X19 or X6 != X14 or X3 = a12 or X9 != a13 or X16 != X1 or X15 != a14 or X17 = X2) and (X16 != a14 or X17 = X2 or a11 != a5 or a7 != X9 or X5 = a7 or X14 != a20 or X7 = a1 or a13 != a14 or X8 = a1 or a16 != X15 or a20 = X18 or a17 = X17 or X15 = a12 or X15 = a20 or a10 != X7 or X4 != X9 or a15 = a17 or X16 != a8 or X2 = a14 or a18 = a12 or X4 != a19 or X11 != X6 or a9 != a6 or X5 != X20 or X9 != X8 or a18 != a6 or false or X8 = a3 or a3 = X14 or X2 = X19 or a7 = X5 or a1 = a14 or a15 != X9 or a17 != X15 or a2 != X6 or X19 = X8 or a8 = a12 or X19 = a12 or X10 != a11 or X6 = a6 or X16 != X13 or X1 != a4 or a2 = a10 or a16 = X18 or X3 != a5 or a11 != a20 or X19 != a18 or X16 = X6) and (X18 = X10 or X1 = X10 or X16 = a6) and (X15 != X12 or X20 != a2 or X18 = a8 or a6 != X10 or X4 != X12 or X18 = X2 or X14 = a15 or X9 != a16 or X13 = X16 or X17 = a12 or a6 != X6 or a11 != X5 or a12 != X18 or a16 = a7 or X1 != a5 or X13 = a4 or X10 != X11 or a8 != X15 or X11 != a20 or X9 != X20 or a9 != X19 or a2 = X5 or X6 != X20 or a6 = a16 or a17 = a5 or X10 = a11 or X4 != X15 or X1 = a5 or X16 != a17 or a8 != a1 or X8 != X2 or a7 = a12 or X19 != X12 or a5 != a2 or a5 != a15 or a13 != a9 or a13 != X20 or a11 != a1 or X17 = a2 or false) and (X15 != a18 or a5 = a14 or a17 = a12 or X20 = X8 or X1 = a1 or X7 != a14 or X15 != X3 or X9 = X1 or a2 = a20 or a3 = a10 or false or a2 = X16 or X17 != X1 or a2 = a8 or a10 != a19 or a13 = a18 or X16 = a11 or X11 = X13 or X9 != X5 or X1 = a2 or X8 != a11 or false or a17 = a5 or X16 = X15 or X3 != a10 or a16 != X1 or a3 != a18 or a11 != a9 or X12 = a16 or X15 = X20 or a1 != a6 or X4 = a12 or a16 = X14 or X6 != X18 or X8 != X11 or X14 = a18 or X2 != X6 or X6 = a14 or a10 = a9) and (X10 != a10 or a8 != a1 or X17 = X12 or X17 = X10 or X11 != a17 or a1 != X12 or X15 = a14 or a3 = X5 or a7 = a8 or X17 = a16 or a2 != X3 or a1 != X15 or true or X12 != a14 or X2 = a8 or a17 != a13 or a2 = X17 or X17 = X18 or a2 != a20 or a8 = X14 or X9 = a4 or X12 != X7 or a5 = a7 or X11 != X4 or X3 = X6 or X14 = X16 or X18 = X20 or X16 = X20 or a12 != a15 or a3 != X20 or X7 != X18 or a8 != X6 or X14 = X8) and (X3 = a16 or X2 = a19 or a18 = a12 or a14 = X12 or a9 = X18 or X16 = a4 or a20 = a7 or a20 != a6 or X2 != X8 or X3 != X11 or X7 = X9 or X10 != a13 or X17 != a2 or a7 = a20 or X19 = a17 or a8 != X4 or X5 != X10 or X15 != X18 or X3 != a11 or X6 = X17 or a14 != X1 or a5 = a3 or X5 != X19 or a19 = a5 or a1 = X17 or X14 = X9 or a2 = a18 or X4 = X17) and (X16 != X6 or a3 = X4 or a14 = X3 or X9 = a13 or X12 != a19 or a9 = a7 or a9 != X1 or X9 = a14 or a8 = a9 or X9 != X14 or X12 = a13 or a18 != X8 or a19 = a10 or X9 = X17 or X15 != X2 or X8 = a10 or X17 = a7 or a19 = X20 or a7 != X12 or X6 = a16 or X14 != X6 or X3 != X10 or X16 = a20 or X5 = a16 or a20 = a19 or X10 = X15 or a5 != a12 or a4 != X7 or a11 != X19 or a15 != X12 or true or a5 != a1) and (a2 != a15 or a18 = X20 or X17 = a6 or a17 = a9 or a11 != X6 or a13 != X6 or X20 != X6 or a13 != a19 or a9 = X5 or X16 != X11 or X15 = a2 or X15 = a8 or a13 = a11 or X18 = a2 or X3 != a4 or X8 != a17 or true or X14 = a11 or a12 = X14 or X19 = X16 or X13 != X16 or a12 = a4 or X19 != X20 or a5 = a4 or X3 != a4 or X4 = X18 or a2 != a5 or X14 = a13 or a9 = a14 or X16 != X3 or X15 != X7 or X2 != a6 or a10 != X11 or X3 = a8 or a19 = X14 or X19 != a1 or X18 != X2 or a3 = a20) and (a16 != X18 or a9 != X11 or X2 != X6 or a16 != X2 or X9 != a1 or a15 != a8 or a11 = X20 or X17 = X8 or a4 != X1 or X12 = X7 or a4 = a9 or a2 != a1 or X10 != X6 or a18 != X11 or a19 != a12 or a2 = X1 or X4 = X20 or a20 = a17 or a11 = a15 or X2 = X8 or a18 = X11 or a9 = X4) and (a5 != X1 or X20 != X19 or X8 != a1 or a11 = a9 or X18 = a3 or a17 != a11 or X19 != a18 or a5 = a12 or X10 = X13 or a10 = a2 or a2 = X15 or a15 != X10 or a16 = X7 or X17 = a13 or false or X3 = X16 or X4 != X7 or a6 != a10 or a8 != X18 or X7 = a20 or a4 = a19 or X20 = X4 or a3 = a12 or a19 = a12) and (a6 = X1 or X11 != a14 or X13 != X9 or a7 = a8 or X16 != a18 or X20 != a1 or a6 != X17 or a3 = X8 or X19 = a8 or X12 = X3 or a5 != X13 or X3 = a13) and (X10 = X2 or X15 != a3 or a5 != X11 or a13 != a20 or X4 != X5 or X1 = X7 or a1 != a13 or X7 != X8 or a20 = X10 or X8 != X1 or X2 = X1 or false) and (X17 = a11 or X6 != a8 or X12 != a7 or X11 != a2 or a13 != a7 or X1 = X20 or a7 = X2 or false or X11 != X4 or a17 = a5 or X10 = X8 or X16 = a11) and (a7 = a20 or X8 != X9 or a8 = X15 or X12 = a17) and (X12 = a16 or X2 != X7 or a20 = X18 or X11 = a2 or X9 != X1 or X7 != a7 or X3 != X20 or X12 = a3 or a10 = X12 or a5 = X11 or a11 = a9 or X8 != X5 or X11 = a1 or X11 != X2 or X6 != X18 or a6 = a10 or X12 = a4 or X19 = a8 or X12 != X6 or X15 != a18 or X10 = a1 or true or a20 != a2 or a14 != a20 or a3 = a8) and (a18 = X6 or X8 != X12 or a11 = a14 or a5 != a4 or X7 != X12 or X10 != a9 or X20 = a8 or X17 != X13 or a8 != a7 or X4 != X12 or a16 != a4 or a3 != X15 or a15 = a6 or true or a12 != a4 or X10 = X17 or X10 != a9 or X12 != X8 or X12 = a1 or a1 != a5 or X2 = a14 or X19 != a4 or a2 = a12 or a16 = a1 or X17 != X11 or a8 != a6 or a14 = a5 or X7 = a17 or X20 != a5 or a14 != X12 or a1 != a19) and (a20 != a4 or a1 = X16 or X17 != a14 or a1 = a15 or X15 = a15 or a12 = X4 or a20 != a9 or a5 != X7 or a12 != a3 or X6 != X13 or X16 != a13 or X10 != X9 or X13 != X2 or a3 != X9 or a8 = X6 or a12 = a10 or X15 != a16 or X9 = a4 or X5 = a17 or a6 = a11 or X18 = a2 or X17 = a1 or X2 != a11 or a1 = X12 or X12 != a17 or X11 = a11 or X13 != a20 or X4 = a7 or a7 != X18 or X10 = a18) and (X5 != a4 or a16 != X11 or X7 = X3 or a6 != X3 or a6 = X16 or a5 = X14 or a8 != a19 or a14 = a2 or a2 = a16) and (a7 = a11 or X19 != X16 or X17 = a2 or X17 = a2 or X1 != X11 or a9 = X6 or a5 != a14 or a15 = X9 or X1 = a5 or a20 != X4 or X19 = a1 or a19 != X12 or a2 = X4 or a15 != X20 or X20 != a8 or a9 = a8 or a16 != X1 or a3 != a4 or X12 != X20) and (X15 != X3 or a18 != X19 or X2 != X16 or a11 != X2 or X13 = a6 or a12 != X3 or a14 = a19 or X7 = X19 or X14 != X10 or a11 = a9 or a19 != X7 or a16 != a7 or a11 != a12 or a7 != X11 or X2 != a12 or X5 != X13 or X8 = X18 or X9 = a9 or a12 != a1 or a18 = a13 or X5 != a10 or X9 != X20 or a10 = a7 or a3 = X13 or X4 != X15) and (X9 != a4 or a4 = X19 or X19 = X3 or a6 != a17 or X11 != X1 or a15 = X16 or a8 != X11 or a18 = a7 or a16 = a18 or a20 != X13 or a1 = X20 or X16 != X5 or X10 != X2 or a19 = X18 or X4 != X17 or a18 != X18 or a15 != X12 or X3 != a2 or a17 = X9 or a10 = a9 or a6 != a12 or a15 = a20 or a11 = X16 or a4 != a15 or a11 != X20 or a10 = X15 or X9 = X7 or a9 = X3 or a2 = a5 or a1 != X19) and (a11 != X10 or X12 = a20 or a4 != X9 or X1 = X16 or a3 != a7 or a12 != a13 or a18 = a20 or X14 = X12 or X20 != a17 or a12 != a1 or X8 = a18 or X10 = a4 or X3 != a12 or a11 = a18 or X8 != a1 or X11 != a5 or a3 != X19 or X19 != a13 or X5 != X9 or X7 != X19 or a1 != a13 or a1 = X10 or a6 = a14 or a10 != X13 or X2 = a10 or a20 != X2 or a6 = a7 or true or X16 = X11 or a3 != a5 or a7 != X6 or X18 = a2 or a15 = X10 or a5 = X12 or a19 = X13) and (X20 != a7 or a2 = X5 or X3 != X6 or X8 = X5 or X13 = X8 or X20 = X17 or X17 != X20 or X19 = a3 or a9 = X10 or a16 = a13 or a16 != a6 or a11 = a2 or X18 != a10 or a5 = a2 or a4 != a3 or X2 != a11 or a16 = a6 or a13 = a12 or a12 = X2 or X16 != X1 or a18 != a10 or X13 != a7 or a19 != a9 or X8 != a12 or X17 != a15 or X3 = X11 or X8 != X16 or X11 = a11 or X10 != a11 or X4 = X14 or X14 != a19 or X19 = a9 or X11 != X14 or a17 != X20 or X7 = X12 or X15 = a4 or a5 != X4 or X6 != X10 or a17 != a11 or X14 = a14 or a14 = a11 or a15 = a8 or a7 = a2 or X15 != a16 or X9 != a7 or X11 = X12 or a15 = X7) and (X13 = a10 or a12 != a17 or X14 != a17 or a3 != a18 or X12 = X1 or a6 = a13 or X19 != a17 or a19 = X5 or X2 != X13 or a1 = a18 or a16 = X10 or X9 = X19 or X3 = X19 or X17 = X14 or a2 = X15 or X20 != X5 or a10 = a20) and (a9 != X1 or a18 = X17 or X4 = X1 or a14 != a2 or X17 = a12 or a14 != X17 or X8 = a16 or a7 = a11 or a9 = X3 or X3 = X1 or X7 != a19 or a20 != X5 or X9 = X17 or X8 = a14 or X1 = a2 or X2 = X11 or X17 != X13 or a14 != X11 or a10 = a1 or X3 = X1 or X20 != a19 or a10 != a7 or a10 != a1 or a1 = X20 or X15 = X12 or X6 = a12 or X17 != a11 or X1 != a11 or X19 = a12 or a19 != a12 or a2 = X12 or X6 = X2 or X10 = X5) and (X9 != X14 or X12 = X1) and (a4 = a1 or a1 = X6 or X11 != a15 or X13 = X6 or a4 != a15 or a13 != X7 or X20 != X2 or X1 = X9 or X16 != X2 or X7 = a18 or X11 = X20 or a9 = X12 or a19 = X12 or X4 != a17 or a8 != X1 or X17 != X9 or a1 != X12 or X9 = a15 or X4 = X5 or X1 = X11 or a4 != X5 or X1 != a20 or X9 != a9 or X12 != a3 or X6 != a5 or a6 = a13 or a4 = a13 or X9 = a4 or X1 != X2 or a14 = X17 or a10 != a9 or X17 != X18) and (a7 != X12 or a4 != X2 or X11 != X5 or X2 != X16 or X17 = a5 or X10 != a15 or true or X9 = a13 or a9 = X13 or X16 != a8 or X16 != a10 or a9 = X16 or X20 != a15 or a15 != X10 or X20 = X15 or a11 = X4 or a12 = a11 or X1 = a1 or a18 = a9 or a14 = a6 or a4 = X11 or X11 = X7 or X6 != X19 or a11 != X14 or X4 = a5 or X8 != X19 or X2 = a13 or X2 = X20 or X12 = X19 or a13 = X3) and (a17 = a8 or a3 != a4 or X3 = a16 or a5 != a16 or X13 != X3 or X3 = X4 or a7 = a15 or X4 = a20 or a16 = a4 or a20 = X14 or a14 = a8 or X2 != a13 or X12 = X2 or X11 != a5 or X17 = X14 or X19 != X14 or a10 = X4 or a12 = X20 or a13 != X8 or X7 = X16 or X4 != a11 or a6 = X8) and (X12 != a20 or X6 = a15 or a18 != X14 or a10 != X7 or X19 = X5 or X7 = a8 or X17 != X15 or X9 = a5 or X20 = X6 or a19 != X10 or a18 != X18 or a10 = a13 or X18 != X10 or X4 = a10 or X8 != X7 or X9 = X2 or X3 = a4 or X5 = a15 or X1 != X2 or a18 != X10 or a13 = a1 or a18 != a9 or a10 != X1 or X12 = a17 or a18 != X20 or a4 != X2 or X5 = X9 or X11 = a1 or a17 != a4 or X8 != X20 or a8 != X14 or X17 = X2) and (X11 = a2 or a17 = X20 or X10 != X15 or X3 = a6 or a7 != X11 or X16 != a11 or a20 = X12 or a9 != a12 or X10 != X11 or X16 != a4 or X20 != a9 or a4 != a12 or X18 = a20 or a15 != a6) and (X17 != a15 or X3 != a5 or X16 != a1 or X18 != X19 or false or X4 = X5 or X15 != a4 or X13 != a15 or X12 = a14 or true or a6 = a17 or a9 != X5 or X7 != X15 or a17 = X10 or X5 != X13 or X8 = X7 or X17 = a20 or X4 = X10 or a10 != X20 or X17 = X5 or X11 != a2 or X16 != a11 or a2 = X10 or a17 = a9 or X1 = X11 or X9 = X19 or X19 != a4) } |",
			"| { ( on X1, X2, X3, X10, X4, X5, X6, X7, X14, X13, X20, X12, X11, X18, X17, X16, X15, X9, X8, X19 ) ( X1, X2, X3, X10, X4, X5, X6, X7, X14, X13, X20, X12, X11, X18, X17, X16, X15, X9, X8, X19 ) | (a8 = a18 or X18 = X5 or a14 = X8 or true or a11 = a8 or a5 != a15 or a11 != a18 or false or a17 != a3 or X18 != a13 or X17 != a8 or true or a12 = a1 or a14 != X18 or X8 != X2 or a16 != X18 or false or a15 = a7 or a20 = a13 or X13 != a2 or X9 = a7 or X4 = X13 or X9 = a15 or a15 != X7 or a17 != a18 or X5 = a18 or X7 != X2 or a11 = X9 or a3 != X15 or X7 = X17 or X16 != a14) and (X5 = X4 or a1 != X6 or a11 = X12 or X3 = X15 or a17 = X20 or a15 != a18 or X17 != a14 or a17 != a8 or X10 = X5 or X16 != a5 or a17 != a12 or a20 = X14 or a15 = X19 or a1 = a7 or a10 = X7 or a17 = a15 or X18 != X1 or a16 != a8 or a10 = X20 or a3 = a9 or a7 = X2 or X10 != X5 or a10 = X5 or a14 != X7 or X5 = X10 or X18 != a1 or a19 = X1 or a16 = X1 or X2 != X3 or a14 != a15 or a1 = a5 or a3 = X14 or X12 != X3 or a17 = X16) and (X4 = X1 or X3 != a2 or a15 = a2 or a10 != a4 or a7 != X10 or X2 != X17 or a5 = a3 or X17 != X3 or X9 = a1 or a17 = a8 or a17 = X11 or a4 = a20 or X18 != a3 or a10 = a6 or a12 != X2 or X18 = X13 or X5 != a10 or a4 = a6 or a19 = a3 or a16 != a12) and (a16 != a14 or X10 = a8 or X13 = X2 or a18 != X14 or a2 != a4 or X14 != X20 or X4 != X8 or X6 = a12 or a11 != a9 or a7 = a15 or X1 != X6 or X7 != a2 or a4 = a11 or X6 != X11 or X6 = a2 or a18 != a10 or X10 = a14 or a2 = X3 or false or a19 != a7 or X1 = X5 or a14 != X9 or a12 = X13 or X4 = a14 or X15 = X1 or a15 = a7 or X16 != a6 or X15 = X9 or a7 = X13 or a8 = X17 or a3 = X6 or X19 = a17 or X2 != X16 or a2 = a5 or false or a10 != X12 or X12 != a6 or a13 = a3 or X17 != X8 or X2 != a18 or X2 != X6 or true or a4 = a9 or X5 = a4 or X4 != X9 or a4 = a18) and (X18 = a3 or a6 != X19 or a2 != X19 or a17 = a9 or X7 != a8 or X16 = X4 or a5 = X19 or X11 = X18 or X16 = a20 or X6 = a17 or X1 = X14 or X4 = a14 or a11 != a8 or a10 = X18 or a7 != a8 or X10 = X19 or a3 = a4 or a10 = X17 or a7 = X12 or a7 != X10 or X10 = a1 or X9 != a5 or X8 = a9 or X9 != X18 or a10 != X16 or X10 != X3 or a13 != a17 or a13 = a3 or false or X9 != X2 or a9 != a6 or true or X11 = a16 or X11 = X16 or a5 = X14 or X3 != a12 or X11 != X4 or X7 != a8 or a3 = X20 or a14 != a3 or a20 = X7) and (a7 = a9 or a5 = a4 or X6 != a10 or a14 = X12 or X12 = X9) and (X1 != X19 or X15 != X2 or X15 = a20 or a4 = a6 or X5 != a14 or a2 = X8 or X20 = X17 or X8 = X5 or X15 != X8 or a9 = X5 or X8 = a8 or a17 = a13 or a7 != X7 or a10 != X11 or a14 != X4 or a7 != a10 or a16 != a14 or X6 = X9 or X2 != X18 or X2 = X10 or a5 = a15 or X3 = X16 or X19 != X10) and (X7 = X15 or a4 = X11 or a3 = a15 or a4 != a8 or X12 = X6) and (X17 = X3 or a12 != X7 or X19 != a18 or a18 != a7 or a6 = a2 or a9 != X15 or a6 != X13 or a15 != X15 or X10 != X3 or X11 != a12 or a19 != X15 or X5 != a19 or X6 = a17 or X17 != X13) and (a1 != a15 or X7 != X10 or X1 = a17 or X14 != X15 or X18 = X19 or a12 = a14 or X1 = X10 or X18 = a19 or a10 = a13 or a2 != X7 or X12 != X5 or a15 != a7 or a1 = X8 or a6 = a3 or a15 != a5 or a18 != a6 or true or X11 != X2 or a10 != X4 or X19 = a4 or a4 != X8 or a17 != X13 or a8 != X8 or X17 != a14 or X1 = a2 or a12 = a8 or X11 != a20 or false or X20 != a4 or a6 = a3 or X9 != a16 or X12 != X1 or a16 = X3) and (X11 != X19 or a17 != X1 or X20 != a13 or X12 != X7 or a7 != X14 or a8 = X11 or a20 != a16 or X10 = X1 or X5 = a1 or X11 = a19 or X13 != a3 or a19 = X18 or a20 = X9 or a13 != X4 or a10 = X17 or X14 != X5 or a14 != a2 or a12 != X8) and (a13 != a5 or X7 = a11 or X12 != X11 or X19 != X17 or a4 = X11 or a12 = a20 or a17 != X11 or X12 != X11 or a19 != X15 or a1 = X11 or a7 != X8 or a4 = a8 or X4 = a11 or X12 = a14 or a11 != X17 or X19 = a13 or a14 = X9 or a8 = a2 or X1 != X19 or X14 = a17 or X5 = a7 or a2 != X10 or X19 = a2 or a1 = X5 or a7 = a20 or a1 = X3 or X19 = X17 or X1 != a18 or X18 != a14) and (X9 != a5 or a9 != X17 or false or X11 = X10 or a17 = a13 or a17 = a12 or X11 != a12 or a17 != a2 or X19 != a14 or X4 = X15 or X17 != a8 or X13 != a3) and (X16 != a3 or a14 = a1 or X10 = a16 or a17 = a18 or X2 = a16 or X3 != a3 or a6 = a9 or a8 != X3 or X10 = X20 or X8 != X3 or a6 != a12 or X19 = a9 or a16 = X20 or X17 = X4 or a18 = a4 or false or a9 = a3 or a7 != X8 or a2 = X3 or a9 != a6 or a3 = X11 or a20 != a2 or a11 != X2) and (X17 != X10 or X8 != a10 or X14 = a19 or X8 != X14 or X17 = X13 or X7 = X4 or a18 != a11 or a18 = X15 or a19 = a17 or X1 != a6 or X17 != X20 or X20 != X17 or a18 != X16 or X17 = X6 or a6 = a5 or X7 != a15 or X1 = X2 or a18 != X18 or X15 = a20 or X15 != a5 or X18 != X3 or X11 != a5 or a17 != a18 or a18 = a16 or a12 = X14 or a3 = a14 or X5 != X17 or X11 != X6 or X16 = X6 or a1 != a3 or X17 != X18 or X14 = a5 or X9 = X5 or X2 != a17 or a18 = X5 or a13 != X10 or X18 = X14 or X18 = a10 or a3 = a19 or a10 != a1 or a19 = a13 or a20 != X19 or a11 = a20 or a12 = X12) and (a6 = X18 or X7 = a17 or X5 != a11) and (a20 != X15 or a1 != X11 or a15 != X11 or X10 != X4 or X6 = X9 or X1 != X16 or X17 != a18 or a3 != X18 or a5 != X16 or a6 = X2 or a2 != a17 or X19 != a4 or X15 = a8 or a14 != X10) and (X18 != X15 or X2 = a7 or a3 != a19 or X12 != a3 or X11 != a14 or a16 != X13 or X10 = a14 or X16 = X18 or X17 != a14 or a11 = X3 or a11 != a7 or a13 != a7 or a11 = X5 or a12 != a10 or X13 != a2 or X19 = X4 or a9 = a15 or X3 != a9 or a3 != X3 or a9 = a19 or X7 = X20 or X13 = a1 or a16 = a20 or X13 != X9 or a2 = a10 or X3 = X8 or a3 != a14 or X18 = X1 or a4 != a20 or a17 != a1 or a3 = a10 or a4 = a13 or a2 = a7 or true or a4 != a9 or X13 = X8 or X8 != X18 or a12 != X3 or a2 = a18 or X15 = X17 or a13 = a5 or X18 = X8 or X2 = a5 or false or X18 = a17) and (X11 != a13 or a7 = a13 or X18 = a6 or a6 != a10 or X12 = X5 or a8 != X19 or X8 != a1 or a18 != a7 or a8 != X13 or a20 = X11 or a5 != a20 or X13 = a18 or X16 = X3 or X2 != a1 or a11 != a3 or a3 = X10 or X11 != a16 or a5 = X12 or X11 = a9 or X1 = X5 or a7 = a2 or a13 = a12 or X6 = X17 or X17 = X1 or a19 = a20 or a1 != a12 or a1 = X13 or X17 != a6 or X20 != X9 or true or X15 = X14 or X2 != a19 or a6 != X11 or X19 = a2 or X20 = a20 or a13 != a10 or X4 = a10 or X15 != a19 or X4 = X14 or a13 = X7) and a3 != a9 and (a4 = X17 or X20 != X11 or a11 != a6 or a2 = X15) and (a14 != X11 or a8 != a10) and (X5 = X14 or a10 != X9) and (X2 != a10 or X20 != a10 or X3 = X6 or a3 != X14 or a10 != a9 or X1 = a11 or a19 != X10 or a3 != a18 or a10 != X7 or a8 = a17 or a17 != a16 or X13 = a6 or X6 != a14 or a6 != a10 or X2 != a6 or a7 != a2 or X12 != X2 or a3 = a6 or X11 = a3 or X7 = X6 or a9 != a1 or a13 = a6 or a11 = X15 or X5 = X12 or a20 = X5 or X20 = X5 or a4 != a11 or a18 != X20 or a2 = X17 or X15 = a19 or a2 != X9 or X3 != a10 or a14 != a10 or true or a1 != X6 or X1 != X6 or a12 = a7 or a18 = X6 or a9 != a11 or X7 = X15) and (a3 != X6 or a8 != X6 or a13 = X17 or X11 != a3 or X17 = X3 or X15 = a13 or X20 = a8 or X14 != a5 or a7 = X3 or a2 != X5 or X4 != X9 or a4 = X10 or a20 = X1 or a7 = a11 or X13 = a5 or a15 = X2 or X1 = X13 or a7 = X19 or X15 != X14 or a14 = X12 or a17 = X17 or X20 = X10 or a2 != X18) and (a1 != X14 or X4 != X3 or a7 = X8 or a9 != a12 or a2 = X9 or a8 != a9 or X8 != X13 or X16 != a16 or X3 != X19 or X8 = X6 or X10 != X15 or a12 != a2 or X16 = X15 or X6 != a11 or a9 = X8 or X8 != X10 or false or a8 = X15 or a17 != a5 or a19 != X9 or a1 = a10 or X13 = X20 or X7 = X8 or X4 = X18 or X3 = X14 or a9 != X15 or X18 = X11 or a6 = a5 or X16 = X14 or X4 != a9 or a4 != a10 or a1 != a17 or X15 != X20 or false or a9 != a11 or X19 != a12 or a2 != X7 or a2 != X4 or X5 != a11 or a18 = a19 or X12 != a2 or a8 = X1 or X17 = a15 or X10 = a2) and (X18 = X15 or X3 != a11 or a1 = a14 or X14 != X2 or a19 != X20 or X18 != a12 or a14 != a6 or X10 = a12 or X18 != a9 or X18 != X3 or a5 != a3 or a14 != a4 or a12 = X5 or X5 != X17 or X10 = X5 or a2 = X12 or X7 != a6 or a10 = a19 or a7 != X16 or false or a15 != X4) and (a17 != X12 or a7 != X7 or a18 = X17 or X1 = X20 or a14 = a8 or X3 = X1 or X6 = a3 or X20 = a7 or a4 != X3 or X13 != a11 or a19 = a13 or X5 = X20 or X17 != a20 or a2 != a15 or X5 = a1 or X9 != X13 or a1 = a10 or X14 = X20) and (a14 != a11 or a2 != a5 or X5 != X19 or X7 = X11 or a13 = a17 or X3 != a4 or X7 = a6 or a14 != a2 or X16 != X4 or a20 != a13 or false or a10 != a19 or X4 != X5 or X17 != X2 or a7 = X8 or X15 != X5 or X8 != a19 or X2 = a2 or X1 = X4 or X13 = a16) and (a9 != X1 or a9 != a11 or X6 = X19 or X15 = X1 or a11 = a5 or a8 != X20 or a2 = a16 or a7 = X10 or a1 != X11 or a13 = X16 or a12 = X1 or a3 != a4 or X3 = X16 or a15 = X10 or X13 = a7 or X10 = a2 or a17 = X11 or a11 = a16 or a9 != X3 or X17 != a20 or a1 != X19) and (X9 != a6 or a20 != X17 or X15 = X16 or X2 != X12 or a6 = a18 or X14 != a10 or a9 != a12 or X14 = X9 or X6 = X4 or X8 = X5 or a10 != a13 or a5 = X16 or X8 != a2 or a12 = a11 or X9 != X18 or X16 != X20 or a2 = X12 or a20 != a16 or a19 = a4 or a7 = a8 or a14 = X17 or a20 = X16 or a15 = a17) and (a3 = X9 or a4 = X19) and (a4 = a16 or a8 != X14 or false or X6 != a11 or X20 = a17 or a13 != a18 or a19 = a14 or a16 != a13 or a16 = a1 or a4 = X7 or X6 != a9 or a6 = X19 or a14 != a9 or a18 = a9 or X17 != a3 or X3 = a20 or a3 = a6 or a7 != X5 or a18 != X7 or X14 != a17 or a16 != X5 or a11 != X17) and (X15 = X20 or a13 = a11 or a6 = a11 or X6 != a17 or a18 != a11 or a18 != X5 or X17 != a15 or a2 != a20 or a15 = a17 or a5 != a8 or X9 != a11 or a20 = X11 or a18 = X20 or X20 != X11 or X13 != a3 or a1 != a8 or a4 = a13 or X3 = a1 or a12 = a11 or a18 = a20 or X8 != X10 or X2 != X6 or X6 = X7 or a15 != a5 or a5 = X2 or a13 = a14 or a1 = a17 or a10 != X4 or X2 = X12 or X10 != a16 or a6 = a9 or a20 = X2 or X10 != a12 or a11 = X2 or X18 != X7 or X6 != X3 or a17 = a5 or X12 != a5 or a18 != a9 or a20 != X11 or a5 != X18 or true or X14 = X4) and (X7 != a2 or a17 != X6 or X12 = a2 or a1 = a3 or a14 = a6 or X7 = X1 or a8 != a7 or a19 != a14 or a2 = X5 or X13 = X8 or a6 = a5 or a1 = a10 or X8 = a1 or a14 = a20 or a3 = X3 or X4 != a7 or false or X10 != X2 or X19 != X4 or a2 = a10 or a9 != a17 or X2 != X14 or X17 != X16 or a3 != X4 or a12 = a10 or X3 = X10 or a5 != a17 or X4 = X12 or a7 != a2 or X4 = a6 or a6 != a16 or a9 = a19 or a13 = X3) and (a1 = X10 or X10 = X18 or X1 != X16 or X19 = X3 or a10 = X9 or a17 = X12 or a14 = X17 or X1 != X2 or false or a9 = X13 or X5 != a20 or a10 != X1 or a13 != a18 or X19 != a11 or true or a2 != a6 or X10 = a3 or a16 != a10 or X1 = X17 or a16 = X14 or a14 != X6 or X11 != a14 or X11 != X3 or a16 = X6 or false or X3 != a20 or a11 != a13) and (X5 != X1 or X12 = X9 or a16 != a18 or a2 = a8 or a12 != a11 or a16 = X4 or X1 != X3 or a18 != X17 or a7 != X3 or a3 = a1 or X13 = X9 or X7 = X13 or X19 = X5 or X6 != X13 or X19 = a4 or X11 = X12 or X8 != a5 or X15 = a20 or X12 = X5) and (a20 = a18 or X14 = X8 or X18 = a3 or a1 != a4 or a17 = X20 or a19 = a1 or X5 = X7 or a14 = a12 or a5 != a2 or a9 = X12 or X5 = a16 or X2 != a4 or a11 != a16 or a16 = a12 or a8 = X19 or X4 != a18 or X2 = a2 or X16 = a14 or X20 = a11 or a8 = a11 or X4 != a20 or X11 = X5 or a10 != a13 or X18 = a8 or X11 = a19 or X9 != X5 or a5 = X12) and (X11 = a5 or a8 != a6 or a13 != a3 or a6 != X19 or X11 = a14 or X14 != X3 or a17 != a3 or a12 = a3 or X5 != a2 or X5 = X8 or a16 = a15 or a14 = X11 or a12 = X1 or X1 != a6 or a20 != a3 or a15 = X20 or X2 = X4 or X10 = X15 or a8 != X19 or X3 = a2 or X2 = a20 or X11 = X7 or X6 != a10 or X6 != X4 or X8 != X20 or a20 = a1 or a18 = a19 or a14 = X7 or a15 != X5 or a4 = a2 or a9 != X9) and (a8 != a10 or a7 != X19 or X5 = X6 or a11 != a18 or X14 != X10 or a8 != a5) and (X13 = a10 or X5 = X11 or a4 = a20 or X13 != X10 or a3 != X3 or a14 = X6 or a8 = X6 or a8 = X5 or X4 = a6 or a20 = X16 or a5 != X9 or a17 != a11 or X4 != X8 or X4 != a9 or a20 != X17 or a14 != X10 or X5 = X6 or a1 != a14 or a2 != X16 or a16 = X19 or X1 != X9 or X19 != X20 or X1 = X12 or X19 != X12 or a5 != a15 or a18 != X17 or X2 != X18) and (a8 = X15 or a3 = a15 or true or a4 = X2 or X2 != a9 or a2 != X11 or X15 != a20 or X17 != X16 or X5 != X19 or X10 = X2 or X5 = X16 or a3 = X13 or a14 != X6 or a13 = X20 or X19 = X14 or X15 != a7 or X14 = X16 or a10 = X9 or a15 != a3 or X19 = X2 or a5 != a16 or X19 = X9 or a1 = a2 or a2 != X8 or X13 = a2 or a1 != X9 or a12 = X20) and (a3 = X14 or a8 = X19 or X14 != X12 or X1 = a20 or a2 = a12 or a9 != X14 or a9 = a3 or X16 = X10 or a15 != a17 or a4 = X20 or X6 = a4 or X13 != X4 or a18 = X6 or a14 != X19 or X10 != a7 or X10 = X9 or X10 != X15 or a12 != a8 or X20 != a8 or X14 != X11 or a9 != a5 or a19 = X9 or a17 = X9 or a6 != a19 or a7 = X4 or X14 = X10 or X5 = X13 or X10 != X2 or X8 = a1 or X16 = X13) and (X3 != X12 or X2 = a5 or false or X17 = a10 or X1 = X2 or X16 = a10 or a5 = X20 or a13 = X14 or a14 = a6 or X5 = a13) and (X5 != a12 or X16 = X19 or X13 = a14 or a9 = X2 or a13 = X5 or X4 = a7 or a13 != a9 or X11 != a11 or X19 = a1 or a19 != X17 or X12 != X19 or a9 != a12 or X19 != a10 or a5 = X4 or X18 = a7 or X1 = a9 or X9 = X6 or a8 = X6 or X3 != X13 or a16 = a4 or X15 != a4 or a3 != a10 or X9 = a8 or a18 != X8 or X16 != X15 or X13 = X11 or X9 = a8 or X2 = a14 or a7 != a13 or a14 != X2 or a1 != a8 or a20 != X5 or X3 = X9 or X3 = X11 or a9 != X15 or X19 = a13 or X10 != a14 or X10 = a12 or X16 = X4 or a2 != a4 or X6 = a12 or X12 != a11 or X12 = X20 or X12 = X1 or X13 != a6) and (X19 = a8 or a14 != a7 or a13 = a18 or X14 = a4 or X10 = X20 or X16 = X1 or a20 = X8 or X6 != a5 or X18 = X1 or a17 = X15 or X11 = X13 or a17 != X11 or a14 = X5 or a10 = X4 or a3 != a20 or X15 != X14 or X15 = X12 or a1 != X17 or a1 != X17) and (a9 = X15 or a15 != a2 or a16 = a20 or a8 = a18 or a10 != a4 or X20 != a14 or a17 != a2 or X20 != X2 or a1 = a5 or a10 != X19 or a17 = X3 or a20 = X16 or a2 != X17 or X12 = a2 or a14 = a1 or a15 = X7 or X3 = X16 or X19 != a19 or X13 != a10 or X4 != X2 or X11 != X9 or X18 != a4 or a1 = X19 or a18 = a13 or a16 != a19 or a1 = a11 or a9 = X18 or a12 = a18 or a1 = X15 or a7 = X14 or a6 = X13 or X19 != a20 or X6 != a4 or a1 != X10 or a13 != a16 or a18 = X15 or a13 = a4 or X19 = a15 or X19 = a2 or X18 = a2 or X20 != X2) and (X20 = X2 or a11 != a20 or true or X7 != X6 or a3 = a13 or X3 != a8 or X18 = X9 or X15 != a14 or a14 != X8 or a4 = a16 or X16 != a9 or X15 != a4 or X11 != a18 or X5 != X11 or X19 != X1 or X7 != a20 or X10 = a18 or a14 != X1 or a7 = X2 or X18 != a11 or X16 = X10 or true or a20 != a6 or a1 != X8 or a8 = X2 or X13 != a2 or true or a13 = X1 or X15 != a4 or a9 != X5 or X19 = X14 or a19 != a10 or X2 = a1 or X9 != X6 or X2 = X5) and (X9 = X18 or X14 = X19 or X4 = a3 or a5 = a20 or true or X4 = a10 or X20 = a14 or a3 != a17 or X6 != X15 or a15 = X11 or X7 != a13 or X14 != X15 or a8 = a5 or a10 = a20 or a3 = a6 or X17 = a12 or a3 = X14 or X19 = a6 or X16 = a17 or X8 = a15 or a17 != a18 or a17 != X16 or a19 = a11 or X6 != a7 or a4 != X8 or X8 != X9 or a6 = X13 or X18 != a20 or a15 != a1 or X2 != X10 or a18 = X13 or a10 = a19 or true or a1 != a10 or X16 = a13 or X11 = a15 or a1 != X3 or X16 != X18 or a1 = X13 or X14 = a16 or X11 != a13 or a13 = a9 or X11 = X9 or a2 = a14 or X6 != a13 or a14 = a11) and (X9 != a8 or X13 = a7 or a7 != a11 or X17 = a6 or X14 = a17 or X5 = X18 or a5 = X20 or a3 = X17 or a6 != X12 or X7 != a2 or a14 != a7 or a2 != a3 or a14 != a16 or X11 = X15 or a9 = a5 or X3 = a20 or X15 = a11 or a8 = a12 or a18 != a17 or a15 = a1 or a15 != a17 or X6 = a14 or X1 = a3 or X13 != a3 or X7 != X5 or a8 = a3 or X1 = a1 or a2 = a20 or a3 = a5 or X2 = a4 or X16 != a12 or X11 = X2 or a8 != X5 or X8 = a4 or X6 = X3 or a20 != X13 or false or a1 = a17 or a16 != a6 or X6 = X14 or X17 = a2 or a6 != a17 or X7 != X15) and (a14 != X16 or a16 != a11 or X13 = a1 or a1 = a2 or a14 = a13 or X14 = X7 or a17 != a6 or a9 != X4 or a4 = X16 or a13 = X8 or X5 = X8 or a5 != a12 or a14 = a10 or X4 != a5 or a20 != X7 or X5 = a5 or a4 = a15 or X15 != X20 or X4 != a1 or X11 = X6 or X13 = X17 or a14 != X7 or a16 != a7 or a12 != a10 or a5 != X6 or X13 = X4 or a11 != X7 or a14 != a8 or a7 = X12 or true or X16 != X7 or X10 = a5 or a9 != X8 or a9 != a12 or a2 = a9 or X18 != X8) } |",
			"| { ( on X1, X2, X3, X10, X4, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X15, X9, X8, X19 ) ( X1, X2, X3, X10, X4, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X15, X9, X8, X19 ) | (a2 = X17 or X7 = a20 or X18 = a8 or a5 != X13 or X19 = a7 or X19 = X14 or a18 = a13 or a16 != X15 or X20 = a14 or X8 != a19 or X7 = a16 or X5 = X7 or a17 != X17 or a5 = a8 or X16 = X1 or X11 != a3 or a6 = X16 or X18 = a3 or X6 != a5 or X6 != X4 or a17 != a6 or a12 != a9 or a8 = a12 or X17 != a4) and (X13 = a14 or X6 != a13 or X9 = X11 or a20 = a10 or true or X10 = X18 or a18 = a19 or a7 != X9) and (a13 = a12 or a17 = a18 or X8 = a17 or X7 != a20 or a8 != a5 or a9 != X14 or X13 != X7 or a6 = a10 or a17 = X11 or X11 = X8 or X14 = X8 or X7 = X17 or a8 = a1 or a2 = a15 or X16 != X2 or a6 != X20 or a6 != X17 or X2 = a4 or a14 = a8 or a20 = a10 or a20 = a16 or a6 != X7 or X16 = a2 or a16 = X19 or a5 != a15 or X13 != X5 or a7 != a5) and (X19 = a6 or true or X15 = X10 or X17 != a9 or X9 != X13 or X3 = X17 or X16 = X18 or X1 = a2 or X19 != X1 or a11 = a2 or a20 = a15 or a7 = a6 or a13 = X3 or X3 = X17 or a5 != a20 or a13 = X4 or a18 = X12 or a14 = a7 or X5 != a13 or X5 = a16 or a1 != a3 or X13 != X20 or a15 != X11 or a15 != X12 or X6 != X7 or X15 != a11 or a15 = a8 or X4 = X16 or a9 = a7 or a16 != X9) and (a4 = X5 or a16 = a20 or false or a17 != X20 or X17 = a16 or X3 != a1 or a7 != X13 or X5 != a15 or X3 != X4 or a12 = a16 or X18 != X5 or X11 = a19 or a19 != a11 or a2 != a6 or true or X17 != X6 or X11 = X19 or X1 != X3 or X16 = a12 or X4 = a3 or a12 = X11 or X3 = X9 or a20 != a7 or X6 != a4 or X10 != a17 or a7 = X14 or X4 != X18 or a5 = a18 or X9 != X17 or X5 != X3 or X5 != X6 or a17 = X2 or X8 = X1 or a17 = a5 or X19 = a11 or a16 != X6 or X12 != a9 or a15 = X12 or X2 = a6 or true or X18 = X20 or a10 = X3 or a16 = X7 or a9 = X14 or a7 = X16 or a9 != X18 or a4 = a13 or a6 != X20 or a4 != X5 or X3 != a3 or X19 = a2) and (a17 != X3 or a19 = a7 or X2 = a13 or a7 != X1 or X12 != X9 or a20 != X11 or X12 != a7 or a12 = a17 or a4 = X17 or X8 != a7 or X20 = a4 or a19 != a2 or a15 != a18 or a6 = X18) and (X14 != X4 or X16 != a16 or true or a4 = X6 or a14 = a2 or a11 = X11 or X4 = a10 or a18 = a4 or a7 != a11 or a4 = X14 or X13 != a2 or X11 = a11 or X3 != a20 or a5 = X13 or X7 = a6 or a11 != X4 or a4 = X16 or a17 != X13 or X17 = a6 or X6 != X4 or a11 = a13 or X3 != a5 or X20 != X12 or a6 = X6 or a18 = X11 or X6 = a1 or false or X18 != a16 or a20 != a14) and (X2 = a19 or a14 = X15 or a5 = X5) and (a9 = X9 or a5 != X20 or a20 = a9 or a15 = a18 or a3 != X18 or a12 != a3 or a18 = a1 or a11 != X12 or X16 = X4 or X3 = X13 or X10 = X11 or X7 != a8 or a1 = a13 or X20 = X6 or X3 != X5 or X14 = X5 or X12 = a2 or X8 != X20 or a12 = X7 or X14 != X10 or a12 != a7 or a4 = a3 or X9 = a19 or a10 = a7 or X9 = X10 or a9 != X11 or a19 = X18 or X11 = a16 or a15 != X6 or a10 != a6 or X20 != X12 or a16 = X12 or X16 != X6 or X5 = X7 or X11 != X5 or X8 != X18 or X9 != a17 or a18 = X13 or a17 != X9 or a18 = X16 or a8 = X7) and (X18 != a19 or a15 = a20 or a3 != a2 or a1 != a8 or X1 != a5 or X18 = X10 or X3 = a11 or X16 != X14 or X9 = a5 or X10 = X14 or a15 = a13 or X14 != a17 or a7 != X16 or X12 = X15 or a16 != a3 or X17 != X4 or a6 != a2 or X19 != X20 or a1 = a7) and (X17 = a13 or X1 != X18 or X9 != X13 or X13 = X3 or a2 = X2 or a11 != a6 or X20 != a12) and (X5 != X7 or a5 = X1 or a8 = a20 or X8 = a3 or true or a1 = a12 or a14 = X2 or a7 = X11 or X17 = a6 or a11 != a6 or X5 != a17 or a7 = a5 or X17 = a10 or X11 = a12 or a13 = X9 or X19 != a5 or false or a15 != X5 or a6 != X13 or X1 != X18 or X8 = a19 or a19 != X10 or a6 != a11 or X18 = X7 or true or X5 = a14 or X9 != X6 or a10 = X9 or X11 = a13 or X6 != X14 or X11 = X20 or X6 != X19 or X12 = a20 or a14 = X10 or a14 != a17 or X19 = a6 or X3 = a15 or a15 = X11 or a3 != X20 or X13 = a6 or a6 != X5 or X16 != X3 or X20 != X17 or a12 = a15 or X18 != a8 or X7 != a2 or a20 = a2 or true or X8 = X10 or a16 != a11 or a10 = a19 or a11 = a17) and (a4 = X9 or a14 = a13 or a4 != X13 or a6 != X3 or X5 = a5 or a12 != a5 or a19 = a7 or X5 != a9 or X10 != X16 or X2 != a4 or a8 != X6 or X4 = a4 or a11 != X11 or a19 = X10 or a10 != a3 or a13 != X9 or a16 = a18 or a12 = X9 or a11 = a6 or X7 = a10 or X19 = X13 or X5 = X2 or X11 = X10 or X13 != X20 or a11 = X11 or a12 = X8 or a7 = a8 or a4 != a20 or X12 != X16 or a13 != X6 or X17 != a15 or a8 = X17 or X4 != a9 or X4 = X1 or a13 = X17 or X18 != X1 or a9 != X6 or a12 = a18 or a17 = a20 or X9 = a13 or false or a15 != X12 or X1 = X5 or X13 = X17 or a14 != X1 or X11 != a10 or X2 = X8 or X10 = a16 or X15 != X16 or a8 != X10) and (a15 != a17 or a8 != X20 or a15 = X3 or X9 = a12 or a14 != X7 or a15 = X2 or a1 = a9 or X9 = X2 or X20 != X6 or a20 != X7 or a17 = X11 or a14 = a9 or a2 != X1 or X5 = a8 or a11 = X15 or a4 = a20 or a20 != X19 or a10 = X6 or a17 != a15 or X16 != X1 or a7 = X2) and (a9 = X9 or a17 = X11 or a12 != X13 or X15 = X3 or a2 != X10 or a17 = X3 or a9 != X4 or X12 != a12 or X18 = a6 or a10 = X8 or a18 != X20 or X12 = a1 or X5 != X19 or a16 != a17 or X13 != X17) and (X3 = a14 or a10 != a11 or a6 = a7 or a3 != a2 or a3 = a20 or X13 = X20 or X9 = X5 or a1 != a14 or a11 = a4 or X1 != X16 or a3 = a2 or X4 = X19 or X13 != X8 or a18 = a16 or X8 = a17 or a12 != a4 or a20 != a5 or a14 != a11 or true or a15 != X9 or X17 = X5 or a14 = a12 or a16 != a13 or X1 = X8 or X10 = a20 or a19 = a7 or X12 != X7 or X15 != a1 or X18 = X14 or X11 != X20 or a2 != a18 or X9 != X5 or X15 != X14) and (a19 != X10 or a9 = X1 or X17 = a12 or a3 != a17 or a15 != X12 or a3 = X20 or a18 = X6 or X13 = X1 or a7 = X12 or a7 = X5) and (X8 = a17 or a8 = a6 or X12 != X5 or a11 != X18 or true or a8 = X11 or a12 = X4 or X1 = X15 or X2 != a12 or a9 != a12 or X8 = a19 or X6 = a1 or a14 = X2 or X14 != a11 or a18 = a4) and (a12 = X8 or a15 = X8 or a20 != X9 or a10 != X5 or X6 = a15 or a3 != a19 or a17 = X3 or a9 = a10 or false or X8 != a20 or a12 != a5 or a13 != X17 or X7 != X17 or a6 != X2 or a4 = X19 or X19 != a5 or a11 != X16 or false or a16 = X15 or a15 = a8 or a2 = a10 or a16 = X20) and (X9 = a7 or X10 = a8 or a19 = a9 or a4 = a19 or a6 = X17 or X7 != a4 or a20 = X6 or X6 = a16 or a8 != a6 or a7 != X9 or a9 = a1 or X10 = X20 or a13 = a10 or X3 != a6 or a1 = a4 or X20 = X9 or a14 != X13 or a5 != X9 or a20 = a15) and (X17 = X7 or X10 != a20 or a14 = a17 or X18 != a20) and (X16 != X18 or X6 != a20 or a5 != a16 or a14 = a2 or X3 != X6 or a9 != X17 or X1 != X3 or a9 != X19 or a19 != X14 or a17 != a6 or X4 != X13 or a14 != X19 or X7 = a8 or X18 != a15 or a20 = a7 or a20 != a5 or a5 = X14 or X6 = X4 or a15 = a19 or X16 = X12 or X4 != a9 or X16 = a12 or a8 != a15 or X1 != X2 or X5 = X2 or a7 = a15 or a18 != a4 or X2 != a20 or X6 != X8 or X4 != X13 or X12 = X18 or a11 = a12 or X5 = X14 or true or a2 = X16 or a6 = a15 or a9 = X12 or a17 != X15 or a8 = a14) and (X19 != a18 or X10 = X5 or X18 = X13 or X10 = X9 or X19 = X3) and (a16 = X3 or X8 = X3 or a7 = a10 or a14 != a1 or a16 = a5 or a18 != X11 or a11 = a1 or a7 != a15 or X1 != a9 or a8 != a9 or a20 = a13 or a15 = X12 or a12 = X9 or X3 = X4 or a15 = X8 or X19 = X7 or X6 != a11 or X20 = a15 or X12 = a17 or a18 = a11 or a17 = X16 or X10 = X1 or X19 != a1 or a9 != X8 or a19 != a7 or a13 = a10 or a3 != X2) and (a15 = X20 or X15 != a4 or X14 != X10 or X8 != X20 or X5 != X7 or a17 = X3 or X13 = X20 or a6 != X12 or a9 = a12 or X7 = a16 or a11 != a5 or X3 = X2 or X4 != a17 or X6 != X16 or a20 = X9 or X4 != X6 or a12 = X4 or a2 = a17 or X6 != X10 or a9 != a18 or a15 = a13 or X10 != X16 or a3 != X10 or a4 != X13 or a17 != a16 or X14 != a4 or X2 != a11 or X5 = a7 or a4 = a11 or X13 != a14 or a6 = X18 or X16 = X20 or a19 = a6 or a2 != a6 or a12 = a18 or a16 != a2 or X8 != X9 or a20 = X14 or X15 != a1 or a5 = a1 or a10 = X18 or a3 = a14 or a19 = X12 or X11 != X6) and (X11 = X18 or a11 != a1 or X2 != a20 or a7 = a12 or a5 != X8 or X15 = a5 or X17 = X12 or X19 != a2 or X20 != X11 or X3 = a10 or X7 != a13 or X11 = X8 or false or X5 != X3 or a11 != a2 or a12 != a11 or a19 = X15 or a6 = a1 or a8 = X14 or X18 = a13 or a11 = X18 or X8 != a11 or a14 != X2 or a12 = a5 or a18 = a1 or a1 != X14 or X15 = X20 or a4 = a3 or X17 = X11 or X1 != X20 or a8 = X18 or X9 = a13 or X14 = X15 or X19 = X20 or a14 != X6) and (a7 != X1 or a9 = a15 or a12 = X9 or a13 = X3 or X12 = a17 or a19 = a4 or a16 != a15 or X15 = a16 or a10 != X7 or false or a20 = X5 or a10 != X19 or X20 != X7 or X14 != X3 or a18 = a6 or a6 != X4 or X5 = a6 or a1 != X6 or a1 != a16 or a6 = a5 or a8 = X11 or a9 != X7 or a14 != a19 or true or a16 != a1 or X8 = a15 or X14 != X13 or a14 != a6 or X7 = a12 or X12 = a14 or a9 != X17 or a11 != a1 or a11 != a10 or a2 = X8 or X5 = X9 or X12 != X2 or true or X13 = a13 or X12 = a3) and (a16 = X16 or X10 != X19 or X6 != a17 or true or X9 = a13 or a7 = a9 or a16 != a8 or X9 = X8 or X16 = a16 or a4 = X18 or a19 = X10 or a8 = a6 or X5 != X10 or a2 != X8 or X8 != a19 or a12 = X8 or a14 = a5 or X19 = a6 or a3 = X17 or a18 = a5 or a2 = a6 or a19 != X10 or a12 = a6 or X4 != X14 or X12 = a4 or a6 != a11 or a17 = a9 or a7 = a1 or a13 != a10 or X3 = a18 or X6 = X4 or a19 != a13 or a19 = a2 or X9 != a14 or X16 != a9 or a17 = X2) and (a4 != X18 or X1 != X9 or a11 != a14 or a8 != a14 or a6 = X9 or X17 != a14 or a11 = X14 or X3 != X6 or a11 = a9 or a17 = X4 or a13 = X15 or a9 != X20 or X9 = a4 or a19 = X4 or X6 != X4 or X10 = X20 or a9 = X14 or X19 != a11 or a7 = X8 or X8 = X20 or X2 != a15 or a17 != a15 or X7 = X15 or X4 != a2 or X5 != a10 or X16 != X1 or X12 != X20 or X17 = a4 or a2 = X15 or X17 != X11 or a14 != X19 or X10 != a2 or X20 = a13 or a12 != X6 or a10 = a2 or X9 = a2) and (X14 != a15 or X7 != a19 or X9 != X15 or a6 != a8 or X16 != X11 or a13 != a19 or a6 = a4 or a2 = a4 or X3 != a3 or a20 = a17 or X5 = a9 or a8 = a10 or a9 = a5) and (X5 = a20 or X4 = a6 or a5 != a7 or X3 != a1 or X14 = X13 or X5 != a5 or a5 != X6 or a15 = a14 or a5 != a20 or X3 = a11 or X4 = a19 or X19 != X20 or X5 = a1 or X7 != X19 or X6 = a14 or a13 = X9 or X2 = a20 or a8 = a14 or a10 = X5 or X13 != a17 or a15 != X6 or X8 = X7 or a17 != X5 or X14 != X7 or X11 = X20 or X1 = a3 or X4 = X16 or a18 != a17 or a17 != X8 or a9 = a18 or X20 = a18 or X13 = X18 or X16 != a7 or a14 = X10 or X6 = a12 or X9 = X15 or X16 != X20 or a5 = X17 or a5 = a12 or X4 = a2) and (X18 = X15 or a19 != a6 or X20 = a1 or X18 = X5 or a15 != X12 or a4 != X20 or a13 = a18 or a13 = X17 or X6 = a8 or X4 = X10 or a2 != X9 or X8 = a11 or a11 = X6 or a10 = X9 or a3 != X4 or X15 = X8 or a11 != X4 or X18 = a16 or X13 = X20 or a14 != a16 or a10 = X15 or a18 != X6 or X8 != a16 or X17 = X1 or X8 != a10 or a17 != a13 or a10 = X13 or a8 != X15 or X6 != a12 or a18 = a10 or X14 = a8 or X12 != X5 or X19 = X2 or X1 != X12 or X13 != X2 or X1 = X18) and (a4 != a16 or a16 != a5 or a16 != X13 or a20 != X1 or a6 = X7 or a9 != a10 or X18 = a2 or X19 = X4 or a11 = a8 or a10 = a13 or a19 != X17 or X3 = a15 or a15 != X7) and (a20 != X18 or X5 != a2 or X2 != a19 or a11 = X14 or a6 = X16 or a5 = X16 or a7 != X5 or a17 = a19 or X12 = X18 or X5 = X18 or X10 != a7 or X18 != X5 or X13 = X5 or X3 != a17 or a15 != a14) and (X9 = X18 or X11 != a8 or a10 != a13 or X19 != X3 or X10 = X4 or a3 = X4 or a11 = a14) and (a7 != X13 or a3 != a5 or X5 = a15 or a5 != X15 or X14 != X13 or a17 = X11 or a16 = X13 or X17 = a5 or X17 != a20 or a3 = a6 or a16 = X5 or a8 = a19 or a11 = a9 or X13 = a12 or X15 = a6 or a6 != a12 or a12 != X8 or X8 = X12 or a5 = a19 or a8 != a6 or X5 != a17) and (X5 = X2 or a5 != a19 or a20 = X7 or X16 != X11 or X19 != X9 or X19 = X18 or X6 != X20 or X12 != a7 or a7 = X13 or a16 = a17 or X5 = X4 or a11 = a20 or X3 = X10 or X6 != a19 or a18 = a3 or X7 = X14 or a13 = a8 or X11 = a2 or a8 != X18 or a20 != X8 or X1 != X14 or a14 = a1 or a5 = a12 or a16 = X5 or X12 = X17 or X3 != X2 or a8 != a10 or X9 != X1 or X7 = X5 or X9 = X12 or a16 != a3 or X7 = a16 or a12 != a20 or X7 = a8 or X8 = X17 or X20 != a10 or a7 != X10) and (a8 = X8 or a4 != a15 or X9 = X11 or X11 = X4 or a13 != X12 or a10 != X8 or X12 = a8 or a9 != a2 or X8 != a18 or X11 != a8 or X20 != a12 or X5 = a8 or X6 != a2 or a18 = X16 or a4 != a1 or a10 != X5 or X19 != a9 or a7 = X17 or a19 != X10 or a7 != X16 or true or X13 = a2 or true or X7 = X20 or a12 = a15 or X19 = a8 or a16 != a5 or X8 != a11 or X7 = a4 or a4 != X1 or X13 = a8 or a15 = X6 or a12 = X17 or a14 != a17 or a18 != X16 or X3 != X4 or X8 != X19 or a4 != a5 or a9 != a8 or a16 != X6 or X13 != X20 or X17 != a10 or X3 != a15 or X10 != a4 or X17 = X12 or false or X8 = a1 or a6 = a1 or X12 != X11 or a1 = a9 or X5 = a18 or X13 = a17 or X15 = X13 or X19 != a3) and (a16 != X13 or a9 = a6) and (X18 != X10 or X11 = X14 or a7 = X9) and (a12 = X18 or X4 = a15 or X19 = a1 or X12 = a3 or X19 != a12 or true or X17 = a20 or X2 != X17 or a8 = a11 or X3 != X4 or a4 = X3 or a3 != X19 or X6 != a10 or a12 = a3 or a11 = a15 or a8 = X4 or X3 = a11 or a10 != a13 or X3 != X12 or a18 != a12 or a4 = X18 or a16 != a4 or X10 != a8 or false or a19 = a20 or X16 != X2 or a19 != a8 or a1 = a14 or a6 != X15 or X16 = a12 or X1 = a2 or X7 != X11 or a8 = X7 or a15 != a12 or a8 = X10 or a11 = X16 or X13 = X10 or a19 = a8 or a3 = X16 or a18 = X20 or X11 != a14 or a4 != X6 or true or a8 != a12 or X20 = X9 or X5 != X7 or X5 != a5 or a2 != a6 or X8 = X3) and (a14 = X1 or a19 = a11 or a6 != X13 or X8 != a6 or X10 != X6 or X10 != X1 or X6 = X19 or a16 = a7 or a5 != a18 or X2 = X12 or a17 != a6 or a2 = X3 or a7 != X9 or a18 != X5 or a2 = a5 or a7 = X6 or a17 = a10 or a16 != X5 or X13 = X7 or a3 != a10 or X20 = X17 or a14 != a10 or X19 = X16 or X16 = X10 or a2 = X16 or a15 = X1 or a10 != X6 or a15 != a6 or X6 != a2 or X17 = X15 or X17 = a6 or X3 = X13 or X5 = a3 or a14 != X16 or X16 != a16 or a4 = a10 or a4 != a17 or a17 != X3 or a3 != X6 or a12 != X17 or a13 != X4 or X20 != X10 or X6 != X8 or X5 = a14 or a20 = a9 or a10 = a16 or X9 != a6 or X9 != a15) and (a16 != X15 or a20 != X5 or a19 = X1 or X4 != X14 or a5 = a12 or a4 != a14 or a12 = X10 or X8 = a8 or X17 != X6 or a13 = a19 or X10 = X11 or a5 != a12 or a20 = a12 or X8 != a8 or X3 != a12 or X3 != X1 or a14 != X15 or a4 != X1 or a3 = a18 or a4 = X12) and (a8 = X1 or a1 != a16 or a14 != X20 or a3 = a20 or a6 = X20 or X3 != a6 or a20 != a17 or a11 = X13 or a18 = X15 or X8 = X18 or a11 != X7 or X9 = a8 or X14 = X10 or a20 = a8 or a2 = X7 or X7 = a18 or a10 = X18 or a13 != X19 or a18 = a2 or X5 != a13 or a11 = X11 or a17 = X6 or X18 = a13 or X13 = X14 or a4 != a19 or X6 = a1 or a9 != a20 or X5 = X17 or X17 != a18 or X16 = X20 or a17 != a10 or X15 = X5 or a18 = X8 or X8 != a11 or X19 != X4 or X11 = X17 or X19 != X12 or a19 = X16 or a4 = a2 or X20 != X4 or X17 != a12 or X20 != X9 or X2 = X16 or a6 = X3 or X8 = X19 or a15 = a2 or a5 != a1) and (a18 != a5 or X16 != a3 or a20 != X16 or X11 != X12 or a20 != a3 or X12 != X19 or a8 != X14 or X20 != a1 or a8 = a19 or X15 != X19 or a19 = a3 or a5 != a8 or X8 = X7 or X20 != a18 or a1 != X9 or X10 = a14 or a18 = a4 or X15 != X14 or a19 = X9 or a15 != X13 or X13 != a4 or a8 != a11 or X18 = a7 or X10 = X19 or a13 = a4 or a5 = a9 or X16 = a2 or X5 != a8 or a6 = a4 or a14 != a10 or a17 != X2 or a17 != X8 or X10 != a11 or X5 != X4 or X14 = a15 or X12 != a16 or X7 = X18 or a10 = X10 or X12 = a13) and (X19 = a20 or a10 != X12 or X3 = X16 or a17 != X13 or X7 = a16 or a12 != X1 or a2 = X8 or a1 = a20 or X6 = X3 or a13 = a1 or X14 != a15 or a4 != a10 or a9 != X6 or X13 = a15 or a10 != X3 or a9 != X15 or X20 = a16 or a15 != X14 or X10 != a5 or a19 = X16 or a10 != a14 or X11 != a8 or X3 != X6 or a8 != X9 or a9 != a3 or X1 != a5 or a3 = a10 or X7 != a17 or X16 = a4 or a16 != X8 or a4 != a2 or X16 != a2 or a14 = a12 or X13 = a17 or X6 != X13 or X5 != X20 or a17 = X4 or X10 = X19 or a13 = X17 or X16 != X3 or a18 = X6 or a4 != X11 or X6 = a14 or X3 != X2 or a11 = X5 or X20 = X3) and (X3 = X20 or a4 = X4 or X10 != a9 or X17 != X10 or a18 != a11 or a3 != a19 or a17 != X13 or X9 != X12 or a9 = a5 or a6 != X9 or X11 != a12 or X8 = X2 or a20 != X15 or X3 != a1 or X19 != X13 or X15 != a2 or a15 != X11 or a14 = a20 or a3 = X19 or X13 != X12 or X1 != X8 or a10 != a16 or X15 != X19 or X5 != X13 or X9 = a19 or X20 = a7 or X14 != X17 or X9 = X15 or a5 != X14 or a15 = a18 or X4 != a8 or a10 = a5 or X4 = X13 or X6 != X15 or a2 != X17 or X17 != a5 or X12 = X19 or X20 = X18 or X14 != a12 or X17 = X1 or a5 = X1 or a15 != X14 or a15 != a19 or X13 != X5 or X4 = X20 or a17 != a9 or a14 != X13 or a13 != a14 or X1 = X7 or X5 = a1 or a4 = X15 or false or X19 = a13) and (false or X14 = X9 or X5 = X1 or X12 != X20 or a7 = X20 or X13 = a15 or X7 = X2 or a13 != a19 or a2 = a18 or X8 = a7 or X15 = X14 or a13 != a17 or a3 != a7 or X10 = X17 or a10 != a18 or a2 != a10 or a3 != a2 or a9 = a5 or X9 = a15 or a13 != a16 or a8 = a18 or X18 = a17 or a9 = X1 or a15 = X18 or X20 != a7 or a19 != X7 or X12 != a15 or a17 = a15 or X11 = a15 or X3 != a9 or X10 = a2 or a10 != X17 or a16 = a9) and (a17 != X5 or X16 != X18 or a19 != X1 or X17 = X16 or X6 != X13 or a2 != a7 or X1 != a13 or a3 = X4 or a18 != a7 or X8 != X18 or X11 = a19 or X18 != a11 or true or a8 = a12 or X9 = a20 or X3 = a14 or a14 != a12 or X3 != X17 or a19 = X7 or false or a2 = a5 or a19 = X10 or X8 = a18 or X10 = X16 or a17 = a8 or a6 != a2 or a20 = X12 or X12 != a13 or false or a17 != X10 or X14 = X6 or a15 = X1 or a6 = X2 or X2 = X18 or X16 != X12 or X9 != X13 or a6 != X12 or a15 != X10 or a11 = X15 or X17 != X7 or a10 != X1 or a18 != a6 or a7 = X3 or a3 != a11 or X10 = X1) and (X18 != a18 or false or a19 != a2 or a4 != a17 or X16 = X17 or X10 = X17 or a1 = X8 or X17 != a8 or X12 = X3 or X19 != X10 or X3 != a5 or X8 != a8 or a15 = X20 or a3 = a20 or a1 = X9) and (a3 = X11 or X6 = a7 or X18 = X13 or X9 = a18 or X1 != X5 or X19 != a6 or a20 != a11 or X5 = a12 or a4 = a9 or a15 != X16 or X16 = a17 or X12 = X6 or X6 = a17 or X11 != a6 or X5 = a1 or a14 = X18 or a16 != a5 or a2 != a11 or X17 != X20 or X2 != a15 or a5 != a6 or X1 = a9 or X16 = a5 or true or X16 != a18 or a12 = a16 or X8 != X14 or X1 != a7 or X12 != X1 or a18 = a12 or a7 = a8 or a18 = a9 or a1 = X2 or X10 = X1 or X19 != a1 or a5 != a3 or X9 = X10 or a7 = X6 or X9 = a8 or X17 = X9 or a11 = a5 or a9 = a20) and (X5 = X12 or X7 = a11 or X20 = a2 or a17 = X8 or a4 != a2 or X13 != a12 or X20 != a5 or a12 != a19 or X19 = a6 or X4 = a2 or X16 != X6 or a14 = a15 or a3 = X18 or X3 = a19 or X20 != X19 or X20 = X8 or X1 != X7 or a13 != a4 or X18 = X19 or X14 = X8 or a5 != a18 or a12 != a18 or a3 != X16 or a14 = a13 or a15 != X16 or a16 != a5 or a8 = a5 or a4 = a19 or X10 != X18) and (X13 != a2 or a7 = X20 or X17 != a14) and (X15 != a18 or X15 = X13 or X12 != X16 or a13 != X3 or a11 = a8 or X2 = X20 or X8 = X6 or X8 = X5 or a8 != X3 or a2 != X5 or a18 != X1 or X8 != a5 or a16 != X1 or a7 = X2) } |",
			"| { ( on X1, X2, X3, X4, X10, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X15, X9, X8, X19 ) ( X1, X2, X3, X4, X10, X5, X6, X7, X14, X13, X12, X20, X11, X18, X17, X16, X15, X9, X8, X19 ) | (X19 != a6 or a20 != a12 or X9 != a16 or a5 != a11) and (a2 = X18 or a8 != a3 or a4 != X5 or a10 = a7 or a10 = X17 or a8 = X3 or a8 != a2 or a20 != X3 or a13 != a8 or X17 = a8 or a15 = a20 or a18 = a15 or X11 = X5 or a8 != X20 or X3 = X17 or X7 = X3 or a13 != a12 or a8 != X16 or X19 != a7 or a19 = a12) and (X6 = a4 or a1 != a13) and (X9 != X11 or a7 = a2 or X8 = a11 or X14 = X8 or X17 = a18 or X11 != a18 or X20 != X7 or X19 = X11 or X8 = X7 or X19 != a9 or a11 = X16 or a13 = a14 or a6 = X12 or a13 != a1 or a2 != a8 or X5 != X13 or X6 != a6 or X15 != X18 or a3 = a13 or X11 != X6 or X18 != a15 or X8 = a8 or X9 = X19 or a2 = a10 or a18 != X4 or a11 != a20 or a11 = a3 or a4 = X8 or X11 != X4 or a3 != X20 or a6 != a3 or a11 != X19 or X20 = X11 or X11 = a7 or X12 = a1 or a20 = X8 or a17 = a20 or X9 = a16 or a5 = X12 or a5 != X10 or X14 != a18 or X3 != X4 or X13 != X11 or X14 != a1 or a16 = X1 or X13 = a18 or a8 = a5 or X3 = X15 or a16 != X8 or X16 != X8 or a9 != a1 or a13 != a17 or X4 = X8) and (X14 = a2 or a10 = X10 or a19 = X4 or X8 != a3 or a12 != X15 or a9 != a4 or X19 = a13 or X13 = X6 or a14 = X16 or X2 != X18 or a8 = X10 or X7 != X1 or a14 != a17 or X9 = a16 or X13 != X5 or a20 = X18 or X9 = X5 or a4 != a19 or a14 != X17 or X17 != a18 or X3 != X6 or X19 = a16 or a8 != a15 or a4 = X9 or a19 = a8 or a11 != a7) and (a8 != a5 or a18 = X19 or a12 != a20 or X3 = X2 or a20 != a10 or X14 != X8 or X5 = a6 or a16 = X15) and (a10 != a18 or a8 = X2 or X20 != a2 or a4 = X17 or a13 != a10 or a4 != X18 or a8 != a7 or a9 = a16 or a10 != a18 or X7 = a13 or X13 != X1 or X13 = X7 or a9 = X17 or X4 = a13 or a15 != X15 or X16 = X1 or a11 != X2 or a6 != a16 or a1 = a11 or a1 != X5 or a17 = X15 or a4 != a10 or X7 != a9 or a20 != a12 or X7 = X17 or a6 = X2 or X12 = X20 or a8 = X13 or a5 = a2 or X8 = a1 or a9 != X2 or X10 = X12 or X17 != a8 or X8 != X1 or a17 = a19 or a4 != a20 or X2 != X4 or a15 = X13 or X1 = a10 or a5 != a3) and (a14 = a3 or X6 != X9 or X5 != X3 or X7 = a15 or a8 = X17 or false or X6 = X13 or X18 = a19 or X1 = X9 or a13 != X19 or X13 = X5 or a7 = a16 or a10 = X17 or X1 != a11 or a3 != X3 or X9 = X8 or a2 = X14 or a4 = a6 or true or X18 != X16 or X3 = a1 or X13 = X2 or a1 != X19 or X15 = X8 or X13 != X11 or a12 = X11 or a14 = X3 or X4 = X2 or a9 != a18 or a7 != X7 or X19 != a8 or X16 != X2 or a8 != X4 or a5 = a1 or a19 != X1 or X9 != a14 or a1 != a14 or a7 != a13 or false or a19 != X11 or X3 != X8 or X5 = X19 or X5 = X10) and (X9 = X11 or X9 != a19 or a10 = a1 or a4 != a12 or a16 = X18 or X13 != a5 or X8 = a12 or X2 = a11 or a4 = X13 or a4 = a12 or a12 = a11 or a4 = X2 or a9 != X2 or X18 = a3 or true or X19 != a5 or X11 = a7 or X12 = a14 or a10 != X17 or a9 != a10 or a20 = X20 or a4 = X6 or a19 != X5 or X12 = X17 or X2 = X12 or X6 = X14) and (a3 != X7 or a7 = a3 or a13 != a2 or true or X5 = a12 or a11 != a13 or a4 != X4 or X17 != X12 or a12 = a15 or a5 = a17 or X11 = a2 or X18 != X7 or a4 = a13 or a4 != X8 or true or X18 != a1 or true or X9 != a7 or a13 = X10 or a7 = X9 or X18 = X14 or a19 != X16 or X18 = X14 or X14 = X12 or a2 != X4 or a16 = X6 or X2 = X15 or a18 != X14 or X20 = X10 or a11 = X12 or a4 = a8 or a14 = a13 or X6 != a2 or a12 != X20 or X12 = a17 or a10 != a20 or a9 != X14 or a1 != X20) and (X18 = X2 or X14 != X5 or a12 != a2 or a14 = a3 or a11 != a17 or X12 != a5 or a20 = a2 or a10 != X9 or X2 != X12 or X10 != X16 or a5 != X19 or a5 = a4 or X4 != X6 or a11 != X4 or a16 != X7 or a19 != X5 or X7 != a17 or X18 != a15 or X20 = a11 or a1 = X12 or X8 = a8 or X6 = a4 or a20 != a3 or X18 = X5 or X3 = X5 or a6 = X16 or X6 != a10 or X11 != a16 or a16 = X10 or X8 = X15 or X6 = a12 or X3 != a5 or X1 != X15 or X14 != a3 or a2 != X17 or X8 != a10 or X9 = X12 or a3 = X2 or a3 = a4 or false or a12 = a18 or X6 != X4 or X15 != a7 or a10 = a9 or a12 != X6 or X3 != a8 or X2 != X20 or X10 != a14 or a11 != X4) and (X3 = a14 or X14 != X4 or a3 != a19 or a12 = X13 or X12 != X2 or X4 != a6 or a14 != a4 or a15 = X18 or X3 = X14 or X3 != a5 or a1 != X20 or a8 != a18 or X17 = X15 or a11 = a6 or a20 = X16) and (X12 != a10 or a18 = X18 or a19 = X19 or a2 = X16 or a5 = a4 or X14 != X18 or a14 != a5 or a4 = a5 or X14 != a13 or a4 != X14 or a2 = X6 or a17 != a11 or a3 != X16 or X19 = X11 or a12 != a1 or a1 != X5 or X19 = X14 or a15 != a17 or X3 = X13 or a15 = X18 or a11 = a7 or a15 = a8 or a12 = X3 or a15 = a16 or a15 != X10 or X15 = X16 or X15 != X3 or X6 != a2 or a7 != X6 or X6 = a11 or X13 != X6 or a5 = a2 or X5 = a12 or X6 != X3 or a14 != X6 or X18 = X3 or X3 != a9 or a18 = X2 or a12 != X9 or X17 = a1 or X15 = a18 or X20 != a5 or a7 = X9 or X16 = X15 or X18 = X2 or X5 != X14 or a5 = a2 or X18 = a2 or X14 = X2 or a5 = X6 or a19 != a5 or a1 != a11 or a11 != X6 or a2 = X18 or X1 = a11 or X1 != a16 or a9 != a14) and (a14 = a3 or a18 != a5 or X18 != X19 or X15 != a9 or a5 = X18 or X7 != a14 or X14 = X1 or a11 != X18 or a10 = a6 or a1 != X3 or X1 = a13 or X10 != X20 or X1 != X15 or a7 = a11 or X11 != X6 or X12 != a13 or X13 = X12 or X8 != a2 or a19 = X18 or a3 != a1 or X11 != a11) and (X17 = a13 or a10 != X4 or a4 != X13 or a15 = X17 or X11 != a5 or false or a8 = X20 or X18 != a6 or X1 = X11 or X13 != a6 or a13 != a1 or X13 != X7 or X8 = a7 or false or X20 = a2 or X1 = a8 or true or X8 = a6 or X7 != X5 or a7 != a18 or a18 = X11 or a4 != a18 or a4 = a9 or X10 = X20 or X11 = X6 or a5 = a20 or a2 = a11 or X16 = a4 or a15 = X2 or true or a11 != X12 or X7 = a7 or X14 = a13 or X6 != X19 or X5 = a7) and (a11 != X4 or a18 != a14 or X10 != X18 or a7 != a12 or a18 = X6 or a3 != a16 or a13 != a20 or X4 != a15 or X12 != X5 or X2 = a4 or X10 = X11 or X10 != a6 or X2 != X16 or X9 != a17 or a18 = a6 or X16 = a16 or a3 = X12 or a2 = X10 or X1 != a9 or true or a14 = a4 or a18 = a1 or a2 != a19 or a7 = X7 or X9 != X19 or a2 = a9 or a12 != X17 or a10 = a15 or X1 != a11 or X7 = a9 or X16 != a16 or X13 = a17 or X17 != a18) and (X3 != a13 or X8 = X2 or a18 != X20 or a4 != a19 or a16 = X12 or a8 = a19 or X12 = X10 or X7 != a8 or a15 = X5 or a10 = X10 or X17 != X8 or a13 = a5 or X10 != a11 or a13 = X20 or X17 = a8 or a10 != X2 or a3 = a13 or X16 = X8 or X6 = X1 or X2 = X19 or X2 != a8 or X4 = X16 or a12 != X20 or X7 = X15) and (X8 = a11 or X10 != X17 or X7 = a1 or X14 != a6 or X3 != a17 or X5 = a9 or X20 != X1 or X15 = X10 or X13 != X9 or X2 != X16 or X19 != X2 or a19 = a14 or a1 = X2 or a17 != X2 or X19 = X4 or X18 != a19 or X15 = X8 or X13 != a18 or X5 = X15 or false or X14 = a12 or X10 != X6 or X14 != a4 or X20 != a3 or X8 != X15 or a17 != a16 or a4 != a9 or X2 != X15 or X13 = X1 or X19 != a9 or X5 != a20 or a1 != X9 or X13 != a15 or false or a10 != X16 or X3 = X14 or X2 != X11 or X11 = X5 or a13 != X17 or X20 = X3 or X6 != X9 or X8 = a10 or X15 != X17 or a18 != a1 or a17 = X12 or a4 != a1 or X10 = X7 or X18 = a13 or X14 = a20 or a12 != a20 or a8 = X1) and (X20 = X18 or X14 != X5 or a7 = X17 or a7 != X4 or X1 != a8 or a12 != a7 or X11 = a16 or a19 != X1 or true or X12 != a1 or a12 != X8 or a11 != a10 or X14 = a3 or a12 != X13 or a18 != X14 or X19 != a2 or X10 != a7 or X9 = X1 or a9 != a17 or X1 = a16 or X3 = a12 or a16 != a6 or X20 != X4 or X1 = X19 or a20 != a1) and (X4 != a15 or a8 != X4 or a18 != X9 or X6 != a15 or X16 = X8 or X19 = X14 or X13 != a7 or a6 = X10 or X14 = X10 or X4 = X1 or X2 != a20 or X15 != X5 or a15 != X9 or a1 != X7 or a17 != X14) and (X11 != a9 or a7 = a4 or X1 != a8 or X15 != X4 or a14 != X6 or a2 != a20 or a1 = X19 or a15 = X15 or X17 != a9 or X17 = X10 or a8 = X17 or X17 = a4 or X6 = X10 or a20 != a5 or X4 = a6 or a11 = X19 or X3 != a17 or X5 = X4 or true or a7 != X3 or a3 = X2 or a16 = X13 or X9 != X5 or a13 != X11 or a18 = a7 or X7 = a5 or a16 != a15 or X2 != X1 or a13 != X14 or a10 = a3 or a1 != a6 or X1 != a13 or a1 != a20) and (a10 != a17 or a8 = X6 or X11 != a14 or X8 = X18 or X9 != a1 or X19 = a1 or X4 != X8 or a8 != X7 or a12 = X20 or true or X14 != a5 or X8 = X4 or a3 != X8) and (a7 = X5 or a6 = a10 or a12 = X10 or X16 != X17 or X7 != X4 or X17 != X15 or a18 != X5 or a1 != a17 or a12 = X16 or X20 = X3 or X15 != a20 or a14 = X2 or a17 != a7 or X7 != X10 or X12 != X3 or X3 = X18) and (a15 = a16 or X3 != a19 or X20 = a10 or X19 != a11 or a20 = X5 or a12 = a19 or X17 = a15 or a17 != X19 or a12 != a20 or X20 != X9 or a13 = X14 or X1 != X2 or X10 = a17 or false or X15 = X6 or a12 != X12 or X8 != X15 or X3 != a2 or X14 = a16 or X9 != X5 or a17 != X14 or a15 != a10 or X2 != a14 or X19 = a4 or X16 != X4 or a12 = a20 or X19 != a4 or X6 != X1 or X9 != a11 or X7 != a6 or X3 = a6 or X11 = X13 or X11 = a18 or X17 = X8 or a1 != X6 or X15 = a7 or a10 != a8 or X3 = a17 or X16 = a14 or X1 = X10 or X15 = X3 or a15 != X13 or X19 != X14 or false or X9 = a13) and (a8 != X18 or a7 != X17 or a9 = a16 or X7 != X12 or X12 = a11 or X15 = X13 or a13 = a3 or a11 != a3 or X10 != X1 or X16 = a18 or a17 != X8 or a5 = X6 or a16 != a11 or X14 != a10 or a4 = X6 or a18 = a13 or X18 = a3 or a9 = a6 or X1 = X12 or X2 != X6 or X16 != X1 or a9 = X11 or X5 = X17 or a10 != X13 or X13 = X2 or X20 = X17 or a9 = X10 or X13 != X15 or a18 != a2 or a5 != X5 or a5 != X1 or a9 = a7 or X2 != a8 or X19 = a4 or a14 = a13 or a11 = X20 or a14 = a18 or a2 = X2 or a19 != a6 or a1 = a6 or X3 != X19 or X12 = a5 or a18 != X1 or a12 != X2 or a8 = a1 or a3 = X6 or X1 != a15 or X18 = X13 or X20 = a16 or X10 != X19 or a2 = a12 or X17 = X5 or X2 != a15 or X16 != a14 or a1 = a18 or X9 != X6) and (X16 != a17 or a7 != X10 or a19 != a20 or X3 = X15 or a15 != a2 or X7 = a16 or a16 = X3 or X9 != a4 or a17 != a2 or a2 = a9 or false or X7 != X6 or a1 = a16 or a17 = a12 or X18 != a20 or a12 != X6 or a11 = a3 or a2 != a15 or X11 != a10 or X18 != a14 or X11 != X18 or X1 = a9 or a11 != a4 or a5 != X4 or a5 != X20 or a6 = a1 or X8 = X13 or X4 = a7 or X8 != X16 or X4 = a6 or a7 = X4) and (X20 != a13 or a7 != X7 or a15 != X10 or a14 = X13 or X18 = X16 or X13 = X17 or X18 != a6 or X8 != a19 or a9 = X18 or X5 = a9 or a17 != a3 or X10 = a9 or X19 != a3) and (X14 != a11 or X11 != X20 or X4 = X1 or a7 = X9 or a20 = X8 or a20 = X15 or a6 != a16 or X13 != X12 or false or X19 = a8 or X4 = X12 or a15 = X17 or X15 != a11 or X16 != a6 or a6 != a13 or a2 != a5 or X10 = a1 or X18 != a2 or X3 != X14 or X13 != X15 or a20 != X11 or a13 != X17 or a7 = X5 or a8 != X10 or X2 != a18 or X5 = a16 or a18 != a13 or X16 = X15 or a19 = a15 or X3 != a5 or X9 != a17 or a9 = a16 or X4 != X5 or X15 = a5 or a17 = X4 or X4 = X6 or false or a11 = a6 or X8 = a8 or X2 != X12 or a11 = X11 or X11 = X10 or X6 != a9 or X13 != X10 or a13 != X14 or a16 = a8 or a2 != a8 or a13 = X1 or X4 = a3 or X15 != X16 or X20 != X8 or X7 = X4 or a15 = a11 or X4 != X6 or X3 = a11) and (a9 = a5 or X11 != a13 or X2 = X11 or X13 = X2 or a2 != X11 or X15 = X12 or X18 = X13 or a10 = a6 or a16 != a19 or X20 = a12 or X8 = a5 or a1 = X15 or true or X9 = a13 or a17 != a15 or a11 = X7 or a8 != a13 or a3 != X11 or a13 != X9 or a8 = X2 or a8 != X9 or a4 = a7 or a6 != X14) and (a3 != X12 or X3 = a6 or a9 != a3 or X9 != X18 or X10 = X6 or X11 != a8 or X13 = a4 or a8 = a1 or a5 != X16 or a17 != a7 or X9 = a15 or X18 != a14 or X18 = X17 or a10 != a20 or a5 != X17 or X7 = X20 or a12 = a4 or X10 != a7 or a14 = X12 or X9 != a13 or X17 = a5 or X18 != X13 or a6 != a14 or X18 = X13 or X5 != X6 or false or a1 = X4 or X19 = a12 or a3 != X4 or a15 = X1 or X12 != X5 or X14 != X7 or X1 != X17 or X18 != a10 or a9 != a20 or a10 != X8 or a16 = a17 or a1 = a20 or a14 != a15 or X13 != a20 or X12 = a3 or a18 != X6 or a6 != a9 or X3 != a15 or a12 != X4 or X19 != X20 or a15 != a16 or a12 = X15 or X14 != a9 or X18 = X19 or false) and (a12 = a1 or X16 = X15 or a1 != a4 or X17 != X8 or a5 = a10 or a5 != X20 or X11 != X1 or a3 != X9 or X10 != X6 or a5 != X2 or X20 = a10 or X2 != X15 or a11 != X16 or a19 != a15 or a11 != a16 or a16 != a1 or X11 != a18 or a2 != a10 or X1 = X13 or X1 != a11 or X13 != X12 or a9 = X17 or X5 = a11 or X18 = X5 or X2 = a15 or a6 != X3 or a6 = a16 or a1 = X9 or X12 != a18 or a18 = a8 or X7 != X16 or X13 != X6 or X20 = a1 or X17 = X4 or a13 != X20 or X10 = a10) and (a9 != X5 or a17 != a12 or a2 = a18 or X8 = a19) and (X16 = a19 or X1 != X7 or X17 = X14 or X1 = a18 or X17 = a13 or X17 = X16 or a4 != a15 or X13 = a5 or a17 != a20 or X8 = X2 or X9 != a16 or a18 = a19 or X10 != a14 or X14 = a4 or a12 = X16 or X7 != X12 or true or X15 != a12 or a4 != a17 or X6 != X20 or X5 != a6 or X5 = a9 or X12 = a2 or X1 = X9 or X17 = a5 or X15 != a15 or X16 != X18 or X15 = a14 or X9 = a15 or X14 = a8 or a20 != X19 or X11 = X5 or a6 = X7 or a15 != X5 or X11 != X8 or a11 = a14 or a8 = X10 or X15 != X8 or X6 != X3 or a1 != a2 or a5 = a1 or a5 != X3 or X15 != X6 or a13 = X10 or X4 != X13 or X15 = a18 or a18 = a11 or a12 != a7 or a6 = X13 or false or a18 != X7) and (a1 = X13 or a19 != X16 or a3 = a5 or X6 = X17 or X16 != a1 or X14 = a18 or a13 = X3 or X11 != a20 or a9 != X3 or X2 = X14 or a7 != X4 or a9 = a2 or X20 != a12 or a10 = X4 or a9 = a17 or X6 != X19 or a18 = a11 or X15 != a15 or X20 != a11 or X2 = a12 or a2 != a12 or false or a17 != a16 or X14 != X12 or false or a6 != X14 or X6 != a20 or X14 != X11 or X18 = a13 or X19 = X14 or a7 = a10 or X4 = a4 or true or X8 != X6 or a16 != a10 or a16 = a8 or a15 != X5 or X15 != a11 or X3 != X11 or X4 = a5 or a3 != X6 or X9 != X20 or a18 != a13 or X11 = a1 or X12 = a15 or X11 != X17 or X16 = a17 or a16 = a9 or a1 != X4) and (a8 = a3 or a2 != a1 or X16 = a5 or a8 != X9 or X17 != X5 or a9 != X2 or a9 = X13 or X4 = X6 or X14 != X10 or X2 = X17 or X11 != X4 or X6 != a6 or a1 = X10 or a16 != X9 or X9 != a6 or X14 != X12 or a17 = a9) and (a16 = a15 or X8 != X2 or a17 = a12 or a15 != X19 or a5 != a12 or a4 != X4 or X3 = a4 or X1 = X11 or a13 = a18 or a16 != a13 or X18 != X10 or X19 != X1 or X9 != X11 or a9 = a13 or false or X17 != a11 or X20 = a10 or X19 = a13 or X15 != X13 or a17 = a14 or X19 = a4 or false or X13 = X5 or X4 = X11 or a2 = a7 or a10 = a16 or X5 = a17 or X4 = a13 or a14 != X8 or a14 != X6 or true or a8 != a10 or X18 = a7 or X2 != X15 or X16 != X3 or a20 != X3 or X7 = X4 or X20 != X6 or X16 = X14 or X20 != a17 or X3 = a12 or X9 != X8 or a5 = X6 or false) and (X12 = X5 or X12 = a4 or a6 = X16 or X10 != a8 or a4 = X12 or a7 != X6 or X12 = a8 or X6 = a19 or a19 = a9 or false or X2 != X1 or X15 != a11 or X17 != a6 or a7 != X5 or a20 != X6 or a10 = a12 or X18 != X8 or a18 != X7 or X18 != a13 or X15 = a6 or a3 = a9 or X4 != X5 or a19 != a11 or X7 = X3 or a20 != a11 or a18 = a8 or X3 != X16 or X19 = a1 or X7 = X3 or a19 = X3 or X17 = X8 or a4 = X9 or X10 != X6 or X20 != a9 or a2 != X16 or X18 != X19 or X9 = X10 or a15 = a6 or a11 != X5 or a11 != a1 or X16 = X13 or X17 = a3 or a3 != a8 or a12 != a10 or X4 != a10 or X15 != X2 or X8 = a8 or a4 = X2 or a7 != a20) and (a20 != a11 or X6 = a13 or a6 = a10 or a1 != a12 or a15 != a11 or X8 = a15 or a11 = a6 or X17 = X1 or a13 != a6 or a13 != a8 or X19 != X15 or a18 != X18 or X17 = X7 or a3 != X2 or X18 != X16 or a11 = a17 or X11 != X10 or X6 != X2 or X15 != a15 or a18 = X8 or X3 != X14 or a13 != a4 or true or X5 = a17 or X20 != a6 or X4 != X9 or X15 = a10 or X5 = a15 or X5 = X14 or X10 = X18 or X1 != X3 or a20 != X13 or a10 != X2 or X16 = a19 or X8 = a14 or X19 != X8 or a11 = X20 or a15 != a9 or a19 = a14 or a1 = X1 or X18 = X2 or a19 = a14 or a12 = a3 or X6 = a10 or a10 != X9 or a1 = a19 or a19 = a6 or X13 != X7 or a6 = a20 or X10 != a13 or a16 != X8 or X1 != a14 or a9 = a16 or false) and (a15 = X11 or a13 = a11 or a8 != X17 or a9 != X7 or a12 != a16 or a12 != a6 or X5 != a14 or X17 = X1 or X20 != a12 or a4 = a19 or X17 = a12 or a11 != a5 or a10 = a7 or X14 != X9 or a19 != a1 or a8 = a3 or false or a11 = X1 or true or a19 != X14 or X4 != a2 or X5 = X18 or a10 != X10 or X8 != a15 or X7 = X2 or a2 != X15 or X14 != a20 or X11 != X1 or X14 != X4 or X18 != X9 or X14 = X11 or a2 = a10 or X15 = a19 or a17 = X12 or a20 != X3 or a8 != X14 or a13 = a17 or X20 = a5 or X2 = a1 or a4 = a5 or X15 != a14 or a11 != X16 or a18 = X14 or a6 = X19 or X10 = X20) and (X13 = a5 or X8 = X15 or X14 != X15 or X1 != a18 or a4 != X1 or a18 != a12 or a6 != a13 or a19 != X7 or X5 != a10 or a3 != X20 or X10 != X9 or X9 = a14 or a1 != X6 or a3 = a1 or a19 = X20 or a3 = X3 or a1 = X4 or X19 != X16 or a17 != X9 or X18 != X20 or X13 = a8 or X14 != X7 or X13 = X2 or X4 != X14 or a3 = X16 or a8 = a9 or X4 != X14 or a7 = a8 or a1 = a2 or a8 != X17 or X13 != a10 or X13 != a18 or a6 = X5 or X19 = a16 or a16 != a5 or X8 != X9 or a13 != a19 or a2 != a5 or a6 != a20 or X11 = a10 or a9 = X13 or true or X3 != X5) and (a5 = a13 or true or a20 = X16 or X13 != X2 or a7 != a17 or a7 != X7 or a4 != a14 or X17 != X16 or true or a1 = X1 or a14 != X11 or X18 = X10 or X9 = X8 or a2 = X3 or a18 = a12 or a4 != a18 or X7 != X3 or a14 = X14 or false or X4 != a5 or a3 = a12 or a15 != a2 or a8 != a20) and (X18 = a1 or X19 = X9 or a7 = a18 or X5 = a20 or X13 = X6 or a7 != X7 or a12 = X14 or X20 = X4 or a4 = X8 or a6 != X11 or a11 = a6 or X16 = X10 or a5 != a17 or a9 = X18 or X8 = a13 or X8 = a3 or a16 = X6 or a2 != X10 or a9 = X19 or X12 = a12 or a14 = a8 or a6 != a5 or a3 = a11 or X2 != X15 or a8 != X15 or a6 = X3 or X13 = a11 or X11 != a2 or a18 = a5 or a11 != a13 or X20 != a4 or X9 = a7 or X8 = a8 or a5 != X15 or a15 != a16 or X17 != a10 or a13 = a4 or a11 != a4 or a20 != X9 or X2 != X16 or a3 != X11 or a8 = X3 or a15 != X10 or a18 != X6 or X18 != a16 or X20 = X13 or X5 = X4 or a16 = a13 or X3 != a1) and (X7 != X10 or X20 = X8 or true or X10 = a16 or X17 = a10 or a18 != a5 or X17 != X20 or X16 != X19 or X18 != a9 or a3 != a14) and (a15 = X12 or a14 != X16 or X4 != X17 or X6 != a1 or X16 != X17 or a12 != X20 or X8 = a1 or X6 != X12 or X4 = a7 or a18 = X15 or false or X4 != X15 or X1 = a9 or X17 = X4 or X6 != a9 or X8 = X4 or a9 != a18 or a13 = X11 or a15 = X17 or X19 = a10 or a14 != X12 or a20 != a1 or a15 = X5 or X1 != X9 or a5 = X11 or X11 != a18 or X9 = X6 or X7 != a15 or X4 = a7 or X17 != a2 or X19 != a4 or X17 != X10 or a1 != X16 or a19 != a20 or X5 = X3 or X17 != X18 or a9 != X4 or X5 = X6 or X6 = X13 or a18 != X15) and (a18 != X7 or a10 = a8 or a6 = X3 or X4 = a7 or a19 = X4 or a12 != X14 or X12 = a11 or X17 != a1 or a5 = a15 or X1 != a14 or a19 = X16 or X10 = a13 or X16 != X20 or X16 = a14 or a19 = X9 or a7 = a4 or a12 != X16 or a3 != X9 or a9 = a6 or X2 = a13 or a7 = X6 or X2 = a15 or a1 = a16 or X7 = a9 or a15 != a9 or a15 != X16 or X2 = a13 or X17 != X12 or X12 = a10 or X19 != X17) and (a3 = X2 or X16 = a8 or a16 != X3 or a19 != X14 or X14 = a5 or X6 = a11 or X14 = a7 or a20 != X12 or X8 != X14 or a10 != a12 or X3 = X15 or X3 = X13 or X11 = X20 or X5 != a5 or X6 = X5 or X8 = a6 or a17 != X12 or a6 != X8 or X10 != a11 or X15 != X8 or a20 != a15 or X10 = X12 or X18 != X1 or a11 != a8 or a16 != a13 or a1 != X16 or X15 != X4 or X17 = X12 or X7 != a8 or X16 = a7 or a2 != a13) and (X19 = X12 or X20 != a2 or a13 = X7 or X11 != X4 or a17 != a5 or X14 != X7 or a6 = a9 or a4 != a12 or X7 = X3 or a2 != X20 or a7 != X14 or X1 != a6 or X7 = a5 or X6 = a14 or X2 = X5 or a2 != a17 or a19 = a17 or a10 = X7 or a5 != a16 or X1 != a13 or X1 != a7 or X12 = X5 or a10 = a11 or X6 = a6 or a19 != a2 or a7 != X7 or a6 != a11 or X17 = a12 or X19 != X10 or a20 != a6 or X3 = a19 or a3 != a7 or X10 != X19 or a13 = a11 or a19 = a4 or a1 != a18 or X15 != a2) and (a8 = X1 or a17 != a18 or a4 != a3 or a18 != X11 or X15 = X10 or a14 != a6 or X7 != X12 or X3 = a8 or X12 = X8 or a4 != X19 or X9 != X13 or X4 = a7 or X15 = a9 or a10 = a15 or a12 != X15 or a16 != X19 or X3 != a18 or a11 = X7 or a1 != X9 or a14 != X3 or a15 != X7 or a8 = a2 or X15 != X6 or X7 = X20 or X1 != X5 or X13 != a8 or X12 = X9 or X20 != a14) and (a14 != a8 or false or X12 != X3 or X16 = a4 or X19 = a4 or a7 = X3 or X10 = a8 or X20 = X1 or a13 != a2 or a20 = a18 or a16 != X5 or a4 != X13 or X12 = a16 or a17 = X2 or a10 != X20 or a1 != X15 or a4 = a11 or X1 = X5 or X15 = a17 or X11 != X1 or a11 = a7 or a11 = a16 or a3 = X11 or a18 = a1 or a18 = X6 or a6 != a12 or a7 != a16 or X14 != X18 or a11 = X14 or X13 != X18 or a11 != X3 or X9 != X6 or X3 != a8 or a7 != a11 or false or a20 = X12 or X16 != X7 or X20 != a15 or a4 != a16 or a3 = X19 or a4 = a17 or a10 != X4 or a4 = X10 or X9 != a16 or X15 = a11 or X20 = a12 or X10 = a17) and (X14 = a2 or a10 = X9 or a15 != a6 or X8 = a12 or X18 = a4 or a16 = X15 or X1 != a18 or a9 = a2 or a10 = X15 or a16 != a19 or a15 = a20 or X8 = X1 or a13 != X15 or a3 = a7 or X14 = X6 or a20 != a1 or a9 = a11) and (a16 = X18 or a14 != a19 or X9 != X2 or a10 != a13 or X15 = X9 or X19 != X16 or a12 != X8 or a18 = a8 or a10 != X6 or a20 != a1 or X16 = a5 or a18 != X5 or a19 = X15 or a6 != a5 or a3 != X1 or a13 != X20 or X20 != a18 or X15 != a1 or true or a2 = X4 or X1 != a15 or X12 != a12 or a4 != a7 or X20 = a3 or X6 = X7 or a7 = a11 or X15 != X17 or a1 = a20 or a4 = a1 or X20 != a6 or a15 = X20 or X4 != a18 or X15 != X10 or a1 != X2 or a11 != a14 or X2 != X15 or a15 != a10 or a6 = X15 or a8 = a5 or a17 != X17 or X3 = X4 or X10 != X8 or a5 = a13 or a14 != a20 or a13 = X2 or X11 != a17 or a20 != X8 or X12 != a2 or X14 != a8) and (X18 != X15 or false or a2 = a15 or X19 != a14 or a18 = a16 or X16 != a16 or X16 != a20) and (X16 = X2 or a10 != X18 or X14 = X2 or X6 = a9 or X17 = a20 or a6 = X4 or a19 != a16 or a13 = X13 or X18 != a16 or X18 != a14 or a6 != a18 or true or a17 != X2 or X9 != a10 or true or false or X16 = a16 or X3 != a1 or a11 != X2 or a14 != X14 or X12 = X13 or X1 = a13 or X18 != X1 or X7 = a13 or X12 = X14 or X1 != a13 or a5 = a10 or a7 = a6 or a17 = a5 or X18 = a14 or a2 != X10 or X16 != X5 or a1 = X4 or a6 != X19 or X4 != X13) and (a10 != a4 or X4 != X12 or a17 = X8 or a16 = a2 or a3 = a11 or X20 = X3 or X18 = X11 or a2 = a17 or X6 = a11 or X15 = X6 or a1 = a20 or X12 = X11 or X13 = a13 or X6 != X10 or X7 = X16 or X17 != a7 or X9 = a7 or a2 = a8 or true or a17 != X2 or X18 != a2 or a1 != a19 or a10 = a18 or a12 != X10 or a15 = X9 or a12 = X5 or X18 = a19 or X5 != a14 or X16 = X15 or X2 != X8 or a17 != a3 or X16 != a13 or X11 != X19 or a5 = X12 or a18 = a11 or X17 = a3 or X4 = X5 or X7 != a19 or a13 = a3 or X12 != X3 or a11 = a2 or a7 = a19 or X12 != X4 or X5 = a5 or X2 != X10 or a20 != a12 or a11 = a15 or X10 != a8 or X10 = a8 or a2 = X19 or a2 = X7) and (X5 != X9 or X8 != a12 or X18 != a9 or a5 = a16 or a8 = X17 or a4 != a13 or a5 = X15 or a13 = X3 or X13 = a18 or X6 != a19 or a14 = X18 or X8 = X7 or X4 = a9 or X20 = X14 or a3 = X9 or X6 = a7 or a7 = X3 or a19 != X18 or X8 = X13 or false or X3 = a10 or a11 != a13 or X2 = X6 or a13 = a16 or X11 != X20 or X13 != a14 or X9 = a12 or X7 != a13 or X2 != a6 or a12 = X13 or a7 != a13 or X12 = X8 or a19 = X16 or a2 = X4 or a1 = a18 or a19 != X12 or X15 != a13) and (a17 = a18 or false or X17 = a13 or a4 = X7 or X8 != X12 or a5 = a18 or X1 = a19 or X1 != X20 or a7 != a16 or a17 != a5 or a6 = X19 or a7 = a10 or a2 != a3 or X12 != X8 or X18 = X9 or a13 = a18 or X10 = X19 or a14 = X12 or X7 != X1 or X14 = X13 or a18 = a6 or a13 = X15 or a12 = a15 or a6 != a14 or a3 = X5 or a17 = X14 or X8 != X9 or X10 != a12 or X4 = a10 or X11 != X9 or X8 = a5 or X2 != a14 or X6 != X9 or a16 != X15 or X4 != a12 or X6 != X12 or X8 != X1 or a1 = X3) and (a20 = X1 or a7 != X8 or a1 != X4 or a8 != X16 or X14 = a19 or X9 = a20 or X4 = X17 or a10 = X3 or a10 != X18 or a1 != X5 or X10 != a4 or a10 != X8 or a16 != a19 or a17 != a12 or X9 = a7 or X18 != X12 or a19 = X4 or a18 != a12 or X7 = a3 or X16 != a19 or a13 != a9 or a13 = a12 or a9 != a2 or X3 != a6 or a3 != X8 or X9 != a4 or a6 != X12 or X8 != X10 or a4 = a7 or X13 = X5 or a19 != X11 or true or a16 = a7 or a12 != X10 or X12 = X8 or false or X14 != X2 or X10 = a8 or X18 != X13) } |",
				
				
			"| { ( on X1, X3, X5, X8, X10, X11, X12, X13, X15, X16, X17, X18, X19 ) ( X1, X3, X5, X8, X10, X11, X12, X13, X15, X16, X17, X18, X19 ) | X16 = X9 and (a4 != a14 or X3 = a11 or X14 != a2 or X4 != X1) and (a14 != a20 or a18 != X5 or a6 = a5 or X13 = a1) and (X11 != X19 or a20 != a10 or a12 = X13) and (a15 != a3 or a5 != X6 or X7 != X20 or X17 != X12 or a1 = a15) } |",
			"| { ( on X1, X2, X4, X5, X7, X8, X11, X12, X13, X15, X18, X19, X20 ) ( X1, X2, X4, X5, X7, X8, X11, X12, X13, X15, X18, X19, X20 ) | (X7 = X12 or a16 != a12 or X4 != X18) and (a1 = a14 or a18 != a11 or a14 != X4 or X1 != X6 or X16 = X14 or X15 != X6) and (X16 = X15 or X6 = X7) and (X2 = X1 or X17 = X19 or X9 != X11 or X9 = a1 or a19 != a9 or X6 = X12 or a18 != X9) and (X12 != a19 or X15 = X9 or X1 != X12) and (a14 != a20 or false or X14 != a1) and (a12 != X9 or X9 != a19 or X1 = X5 or X16 != X14 or X5 != a1 or a2 != X17) and (a6 = X16 or a5 != X19 or X6 != X5 or a14 = a7 or X19 = X20 or a15 != a14) } |",
			"| { ( on X1, X2, X5, X8, X9, X11, X14, X15, X16, X17, X18, X19, X20 ) ( X1, X2, X5, X8, X9, X11, X14, X15, X16, X17, X18, X19, X20 ) | X7 = a17 and X12 != X16 and a9 = X10 and a18 != a3 or X8 = a15 and a20 = X4 and X6 != X14 or X8 != X12 and a2 != X14 or a4 != X6 and a6 = X14 or a4 != a9 and a6 != a12 and a4 = X7 and X6 = a2 <=> (a14 != X7 and X11 != a11 or a4 = X16 or X7 = X19 and a1 != a16 <=> X5 != a2 and X11 != a6 or X6 != X20 and a17 != X9 or X8 != X19) } |",
			"| { ( on X1, X3, X4, X5, X6, X7, X10, X11, X12, X15, X16, X19, X20 ) ( X1, X3, X4, X5, X6, X7, X10, X11, X12, X15, X16, X19, X20 ) | (X12 = a19 and a7 != a5 and X9 != a8 or X10 != X2 or X16 = X14 or X12 != a2 and a20 != a2 and X19 = a17 <=> a13 = X10 and (a1 = a2 or X15 != a20 or X2 != a17) and (a10 != X2 or a20 != a19 or X5 != a20) and a7 != a10) <=> (a7 != a5 and X2 != a17 and (a10 != X17 or X15 = X11) and (X9 != X13 or a10 != X17 or a11 != X18) => X5 != a17 and X19 = a11 or X4 = X2 and X18 = X13 and a11 != a19 or a5 != X3 or a18 = X15 and a11 != a5) } |",
			"| { ( on X1, X2, X3, X5, X8, X9, X10, X11, X14, X15, X16, X18, X19 ) ( X1, X2, X3, X5, X8, X9, X10, X11, X14, X15, X16, X18, X19 ) | (a12 != X18 and X17 != a18 and (X10 = a14 or X9 != X10) and (a11 = X13 or X2 = a2) <=> (X1 != X10 or X19 = a15 or a11 = a20) and (X19 != a5 or X5 = a9) and (X1 != X16 or a15 = X10) and X7 = a20) <=> ((a15 = X17 or X17 = a1) and (a20 = X16 or X7 != a13) and (X6 = X4 or X3 != a8) => X12 != a1 and (a20 = X17 or X16 != X5) and a10 = a17) } |",
			"| { ( on X1, X2, X3, X5, X7, X8, X11, X12, X13, X14, X16, X17, X19 ) ( X1, X2, X3, X5, X7, X8, X11, X12, X13, X14, X16, X17, X19 ) | (X13 = X5 or X1 != a7 or a12 = a5) and (a13 = a7 or X17 = a18) and (X6 != a19 or X14 != a8) and (X3 != X16 or a3 != a1 or X3 != a9) <=> (X1 = X20 and (X17 = a15 or X8 = X1) and (a9 = X8 or X19 != X10) => a17 = a12 and a20 != X11 or a11 != a17 and X19 != X10 or X7 = a10) => a19 != X9 and a16 != X9 and X8 = X7 and X15 = X4 and a14 = X16 or X20 != a17 or X9 = a20 and a20 = a11 and X19 = X4 or a9 = X13 and a3 = a1 and X9 != a13 and a19 != a20 or a8 != X18 and X5 = a20 and a13 = a17 or X1 != X18 } |",
			"| { ( on X1, X2, X3, X7, X9, X11, X12, X15, X17, X18, X19, X20 ) ( X1, X2, X3, X7, X9, X11, X12, X15, X17, X18, X19, X20 ) | (a3 != a19 or X20 != X7 or a15 != a11 or X8 != a9 or a17 = a16) and X5 != a2 and a17 = a3 and (X11 != X18 or X15 = a4) and (X8 = X4 or a1 != X2 or a18 = a4 or a3 != a16) and (a17 != X1 or a16 != a12 or X15 != X20 or a2 = a8 or a2 = X1) <=> ((a16 = a7 and (X8 = a11 or X2 != a10) and (X2 = X11 or X7 != a20) <=> (true or a8 = a6) and (X7 != X15 or a9 = X20) and (X18 = a10 or X6 != X9)) <=> (X5 != X16 or a7 = a11 or a1 != X11) and (X1 != a5 or a7 != X19 or a3 != a15) and X2 != X5 and (a7 != a17 or a13 != a15 or X12 = a17)) } |",
			"| { ( on X1, X2, X4, X5, X7, X9, X10, X11, X12, X14, X15, X16, X17, X20 ) ( X1, X2, X4, X5, X7, X9, X10, X11, X12, X14, X15, X16, X17, X20 ) | a6 != a18 and X11 != a2 and X18 != X13 and a6 != X14 and X8 != X4 and a16 != X11 and a19 != a11 and a8 != a3 and a4 != a12 and a14 != a12 and a12 != a14 and a13 != a1 and X3 != X14 and a9 != a20 and X20 != a6 and a1 != X20 and a12 != a8 and X12 != X4 and a9 != X5 and a19 != X17 and a4 != a6 and X7 != a3 and X19 != X7 and a6 != X20 and X16 != X3 and X3 != X9 and a7 != X1 and a19 != a4 and X3 != X14 and a8 != a17 and X9 != X2 and X7 != X3 and X7 != X4 and a10 != a9 and X13 != X6 and false and a4 != X6 and X7 != X5 and a19 != a9 and X15 != a9 and a15 != a13 and a19 != a2 and X19 != X16 and X11 != X3 and X7 != a14 and a1 != X19 } |",
			"| { ( on X1, X2, X5, X6, X9, X11, X13, X14, X15, X16, X19 ) ( X1, X2, X5, X6, X9, X11, X13, X14, X15, X16, X19 ) | a16 != X18 and X13 != X10 and X18 != X8 and a8 != a11 and X6 != X5 and X6 != a11 and X16 != X10 and a13 != a10 and a8 != X9 and a7 != X18 and a15 != X17 and a4 != a20 and X13 != X9 and X20 != X1 and X4 != a18 and a16 != a9 and X9 != a7 and X6 != X1 and X11 != X16 and a9 != X1 and X1 != X2 and a9 != a11 and a6 != a8 and a18 != X16 and X2 != X8 and X7 != X15 and X2 != X18 and false and a16 != X10 and a16 != a9 and X2 != a4 and a9 != a20 and X13 != X16 and a11 != a18 and X6 != X3 and a11 != X2 and X9 != X18 and X10 != a8 and X17 != a1 and X8 != X14 and a18 != a20 and a15 != X12 and X15 != X14 and a9 != X14 and X10 != a2 and X3 != a4 and a6 != a7 and X9 != X1 and X6 != a16 and a7 != a20 and a1 != a16 and X14 != a11 and X9 != a15 and X2 != X7 and a12 != X8 } |",
		}));		
	}
}
